to_pequiv_matrix_mul'

Stream: new members

[Jamie Reason]

Hey, in data.matrix.pequiv there is a lemma docs#pequiv.to_pequiv_mul_matrix , I wanted to use an equivalent of this lemma but for left multiplication (which requires additional hypothesis that h : f = f.symm).

I've written and proved this lemma,

universe v
variables {m n : Type*} {α : Type v}
lemma to_pequiv_matrix_mul' [fintype n] [decidable_eq n] [semiring α] (f : n ≃ n)
  (M : matrix m n α) (h : f = f.symm) : (M ⬝ f.to_pequiv.to_matrix) = λ i j, M i (f j) :=
by {  ext i j, rw [pequiv.matrix_mul_apply, ←equiv.to_pequiv_symm, equiv.to_pequiv_apply, ←h]}

Is this something worth adding to data.matrix.pequiv or not? And is the naming appropriate?

[Junyan Xu]

Do you really need f = f.symm or you just need to replace one of the two f in the conclusion by f.symm?

[Jamie Reason]

Ah yes, thanks, my use case had f = f.symm so I didn't consider that

lemma to_pequiv_matrix_mul {m n : Type*} {α : Type v} [fintype n] [decidable_eq n] [semiring α] (f : n ≃ n) (M : matrix m n α):
(M ⬝ f.to_pequiv.to_matrix) = λ i j, M i (f.symm j) :=
by {  ext i j, rw [pequiv.matrix_mul_apply, ←equiv.to_pequiv_symm, equiv.to_pequiv_apply]}

[Eric Wieser]

The RHS might be better expressed with docs#matrix.submatrix

[Jamie Reason]

I think that is a slightly nicer result. Although it is not consistent with docs#pequiv.to_pequiv_mul_matrix currently in mathlib

lemma to_pequiv_matrix_mul {m n : Type*} {α : Type v} [fintype n] [decidable_eq n] [semiring α] (f : n ≃ n) (M : matrix m n α):
(M ⬝ f.to_pequiv.to_matrix) = matrix.submatrix M id (f.symm) :=
by {  ext i j, rw [pequiv.matrix_mul_apply, ←equiv.to_pequiv_symm, equiv.to_pequiv_apply, matrix.submatrix_apply, id.def] }