## Stream: new members

### Topic: to_pequiv_matrix_mul'

#### Jamie Reason (Aug 22 2022 at 13:22):

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 (Aug 22 2022 at 21:07):

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 (Aug 23 2022 at 10:39):

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 (Aug 23 2022 at 15:18):

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

#### Jamie Reason (Aug 23 2022 at 16:36):

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] }


Last updated: Dec 20 2023 at 11:08 UTC