case a.h
k : Type ?u.14630
l : Type ?u.14633
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : m ≃ m
M : Matrix m n α
i : m
j : n
⊢ (toMatrix (Equiv.toPEquiv f) ⬝ M) i j = M (↑f i) j
k : Type ?u.14630
l : Type ?u.14633
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : m ≃ m
M : Matrix m n α
⊢ toMatrix (Equiv.toPEquiv f) ⬝ M = fun i => M (↑f i)
ext (i j)
no goals
case a.h
k : Type ?u.14630
l : Type ?u.14633
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : m ≃ m
M : Matrix m n α
i : m
j : n
⊢ (toMatrix (Equiv.toPEquiv f) ⬝ M) i j = M (↑f i) j
rw [mul_matrix_apply, Equiv.toPEquiv_apply]