R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ p : n × n, ↑(algebraMap R A) (M p.fst p.snd) ⊗ₜ[R] stdBasisMatrix p.fst p.snd 1 = 1 ⊗ₜ[R] M
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ invFun R A n (Matrix.map M ↑(algebraMap R A)) = 1 ⊗ₜ[R] M
dsimp [invFun]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 ⊗ₜ[R] ∑ a : n × n, M a.fst a.snd • stdBasisMatrix a.fst a.snd 1 = 1 ⊗ₜ[R] M
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ p : n × n, ↑(algebraMap R A) (M p.fst p.snd) ⊗ₜ[R] stdBasisMatrix p.fst p.snd 1 = 1 ⊗ₜ[R] M
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum, mul_boole]
case e_n
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.fst a.snd • stdBasisMatrix a.fst a.snd 1 = M
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ 1 ⊗ₜ[R] ∑ a : n × n, M a.fst a.snd • stdBasisMatrix a.fst a.snd 1 = 1 ⊗ₜ[R] M
congr
case e_n
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.fst a.snd • stdBasisMatrix a.fst a.snd 1 = ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j)
case e_n
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.fst a.snd • stdBasisMatrix a.fst a.snd 1 = M
conv_rhs => rw [matrix_eq_sum_std_basis M]
case h.e'_3.a.a
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
x✝¹ : n
a✝¹ : x✝¹ ∈ Finset.univ
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ stdBasisMatrix x✝¹ x✝ (M x✝¹ x✝) = M (x✝¹, x✝).fst (x✝¹, x✝).snd • stdBasisMatrix (x✝¹, x✝).fst (x✝¹, x✝).snd 1
case e_n
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ∑ a : n × n, M a.fst a.snd • stdBasisMatrix a.fst a.snd 1 = ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j)
convert Finset.sum_product (β := Matrix n n R)
no goals
case h.e'_3.a.a
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
x✝¹ : n
a✝¹ : x✝¹ ∈ Finset.univ
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ stdBasisMatrix x✝¹ x✝ (M x✝¹ x✝) = M (x✝¹, x✝).fst (x✝¹, x✝).snd • stdBasisMatrix (x✝¹, x✝).fst (x✝¹, x✝).snd 1
simp