[GOAL]
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
⊢ ∀ (a₁ a₂ : A) (b₁ b₂ : Matrix n n R),
    ↑(toFunLinear R A n) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      ↑(toFunLinear R A n) (a₁ ⊗ₜ[R] b₁) * ↑(toFunLinear R A n) (a₂ ⊗ₜ[R] b₂)
[PROOFSTEP]
intros
[GOAL]
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
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ ↑(toFunLinear R A n) ((a₁✝ * a₂✝) ⊗ₜ[R] (b₁✝ * b₂✝)) =
    ↑(toFunLinear R A n) (a₁✝ ⊗ₜ[R] b₁✝) * ↑(toFunLinear R A n) (a₂✝ ⊗ₜ[R] b₂✝)
[PROOFSTEP]
simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_mul]
[GOAL]
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
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ (a₁✝ * a₂✝) • (Matrix.map b₁✝ ↑(algebraMap R A) * Matrix.map b₂✝ ↑(algebraMap R A)) =
    a₁✝ • Matrix.map b₁✝ ↑(algebraMap R A) * a₂✝ • Matrix.map b₂✝ ↑(algebraMap R A)
[PROOFSTEP]
ext
[GOAL]
case a.h
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
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
i✝ x✝ : n
⊢ ((a₁✝ * a₂✝) • (Matrix.map b₁✝ ↑(algebraMap R A) * Matrix.map b₂✝ ↑(algebraMap R A))) i✝ x✝ =
    (a₁✝ • Matrix.map b₁✝ ↑(algebraMap R A) * a₂✝ • Matrix.map b₂✝ ↑(algebraMap R A)) i✝ x✝
[PROOFSTEP]
dsimp
[GOAL]
case a.h
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
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
i✝ x✝ : n
⊢ a₁✝ * a₂✝ * (Matrix.map b₁✝ ↑(algebraMap R A) * Matrix.map b₂✝ ↑(algebraMap R A)) i✝ x✝ =
    (a₁✝ • Matrix.map b₁✝ ↑(algebraMap R A) * a₂✝ • Matrix.map b₂✝ ↑(algebraMap R A)) i✝ x✝
[PROOFSTEP]
simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum, _root_.mul_assoc,
  Algebra.left_comm]
[GOAL]
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
⊢ ∀ (r : R), ↑(toFunLinear R A n) (↑(algebraMap R A) r ⊗ₜ[R] 1) = ↑(algebraMap R (Matrix n n A)) r
[PROOFSTEP]
intros
[GOAL]
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
r✝ : R
⊢ ↑(toFunLinear R A n) (↑(algebraMap R A) r✝ ⊗ₜ[R] 1) = ↑(algebraMap R (Matrix n n A)) r✝
[PROOFSTEP]
simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_one (algebraMap R A) (map_zero _) (map_one _),
  algebraMap_smul, Algebra.algebraMap_eq_smul_one]
[GOAL]
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
a : A
m : Matrix n n R
⊢ ↑(toFunAlgHom R A n) (a ⊗ₜ[R] m) = a • Matrix.map m ↑(algebraMap R A)
[PROOFSTEP]
simp [toFunAlgHom, algHomOfLinearMapTensorProduct, toFunLinear]
[GOAL]
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
a : A
m : Matrix n n R
⊢ AddHom.toFun (lift (toFunBilinear R A n)).toAddHom (a ⊗ₜ[R] m) = a • Matrix.map m ↑(algebraMap R A)
[PROOFSTEP]
rfl
[GOAL]
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
⊢ invFun R A n 0 = 0
[PROOFSTEP]
simp [invFun]
[GOAL]
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 N : Matrix n n A
⊢ invFun R A n (M + N) = invFun R A n M + invFun R A n N
[PROOFSTEP]
simp [invFun, add_tmul, Finset.sum_add_distrib]
[GOAL]
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
a : A
M : Matrix n n A
⊢ invFun R A n (a • M) = a ⊗ₜ[R] 1 * invFun R A n M
[PROOFSTEP]
simp [invFun, Finset.mul_sum]
[GOAL]
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
[PROOFSTEP]
dsimp [invFun]
[GOAL]
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
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum, mul_boole]
[GOAL]
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
[PROOFSTEP]
congr
[GOAL]
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
[PROOFSTEP]
conv_rhs => rw [matrix_eq_sum_std_basis M]
[GOAL]
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
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
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
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
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
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
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)
[PROOFSTEP]
convert Finset.sum_product (β := Matrix n n R)
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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 A
⊢ ↑(toFunAlgHom R A n) (invFun R A n M) = M
[PROOFSTEP]
simp only [invFun, AlgHom.map_sum, stdBasisMatrix, apply_ite ↑(algebraMap R A), smul_eq_mul, mul_boole,
  toFunAlgHom_apply, RingHom.map_zero, RingHom.map_one, Matrix.map_apply, Pi.smul_def]
[GOAL]
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 A
⊢ ∑ x : n × n, M x.fst x.snd • Matrix.map (fun i' j' => if x.fst = i' ∧ x.snd = j' then 1 else 0) ↑(algebraMap R A) = M
[PROOFSTEP]
convert Finset.sum_product (β := Matrix n n A)
[GOAL]
case h.e'_3
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 A
⊢ M =
    ∑ x : n,
      ∑ y : n,
        M (x, y).fst (x, y).snd •
          Matrix.map (fun i' j' => if (x, y).fst = i' ∧ (x, y).snd = j' then 1 else 0) ↑(algebraMap R A)
[PROOFSTEP]
conv_lhs => rw [matrix_eq_sum_std_basis M]
[GOAL]
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 A
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
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 A
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
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 A
| M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M]
[GOAL]
case h.e'_3
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 A
⊢ ∑ i : n, ∑ j : n, stdBasisMatrix i j (M i j) =
    ∑ x : n,
      ∑ y : n,
        M (x, y).fst (x, y).snd •
          Matrix.map (fun i' j' => if (x, y).fst = i' ∧ (x, y).snd = j' then 1 else 0) ↑(algebraMap R A)
[PROOFSTEP]
refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => Matrix.ext fun a b => ?_
[GOAL]
case h.e'_3
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 A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
⊢ stdBasisMatrix i j (M i j) a b =
    (M (i, j).fst (i, j).snd •
        Matrix.map (fun i' j' => if (i, j).fst = i' ∧ (i, j).snd = j' then 1 else 0) ↑(algebraMap R A))
      a b
[PROOFSTEP]
simp only [stdBasisMatrix, smul_apply, Matrix.map_apply]
[GOAL]
case h.e'_3
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 A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
⊢ (if i = a ∧ j = b then M i j else 0) = M i j • ↑(algebraMap R A) (if i = a ∧ j = b then 1 else 0)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
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 A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
h✝ : i = a ∧ j = b
⊢ M i j = M i j • ↑(algebraMap R A) 1
[PROOFSTEP]
aesop
[GOAL]
case neg
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 A
i : n
x✝¹ : i ∈ Finset.univ
j : n
x✝ : j ∈ Finset.univ
a b : n
h✝ : ¬(i = a ∧ j = b)
⊢ 0 = M i j • ↑(algebraMap R A) 0
[PROOFSTEP]
aesop
[GOAL]
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 : A ⊗[R] Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) M) = M
[PROOFSTEP]
induction M using TensorProduct.induction_on with
| zero => simp
| tmul a m => simp
| add x y hx hy =>
  rw [map_add]
  conv_rhs => rw [← hx, ← hy, ← invFun_add]
[GOAL]
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 : A ⊗[R] Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) M) = M
[PROOFSTEP]
induction M using TensorProduct.induction_on with
| zero => simp
| tmul a m => simp
| add x y hx hy =>
  rw [map_add]
  conv_rhs => rw [← hx, ← hy, ← invFun_add]
[GOAL]
case zero
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
⊢ invFun R A n (↑(toFunAlgHom R A n) 0) = 0
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
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
⊢ invFun R A n (↑(toFunAlgHom R A n) 0) = 0
[PROOFSTEP]
simp
[GOAL]
case tmul
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
a : A
m : Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) (a ⊗ₜ[R] m)) = a ⊗ₜ[R] m
[PROOFSTEP]

| tmul a m => simp
[GOAL]
case tmul
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
a : A
m : Matrix n n R
⊢ invFun R A n (↑(toFunAlgHom R A n) (a ⊗ₜ[R] m)) = a ⊗ₜ[R] m
[PROOFSTEP]
simp
[GOAL]
case add
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
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) (x + y)) = x + y
[PROOFSTEP]

| add x y hx hy =>
  rw [map_add]
  conv_rhs => rw [← hx, ← hy, ← invFun_add]
[GOAL]
case add
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
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) (x + y)) = x + y
[PROOFSTEP]
rw [map_add]
[GOAL]
case add
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
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
⊢ invFun R A n (↑(toFunAlgHom R A n) x + ↑(toFunAlgHom R A n) y) = x + y
[PROOFSTEP]
conv_rhs => rw [← hx, ← hy, ← invFun_add]
[GOAL]
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
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
| x + y
[PROOFSTEP]
rw [← hx, ← hy, ← invFun_add]
[GOAL]
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
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
| x + y
[PROOFSTEP]
rw [← hx, ← hy, ← invFun_add]
[GOAL]
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
x y : A ⊗[R] Matrix n n R
hx : invFun R A n (↑(toFunAlgHom R A n) x) = x
hy : invFun R A n (↑(toFunAlgHom R A n) y) = y
| x + y
[PROOFSTEP]
rw [← hx, ← hy, ← invFun_add]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ ↑(matrixEquivTensor R A n) (stdBasisMatrix i j x) = x ⊗ₜ[R] stdBasisMatrix i j 1
[PROOFSTEP]
have t : ∀ p : n × n, i = p.1 ∧ j = p.2 ↔ p = (i, j) := by aesop
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
⊢ ∀ (p : n × n), i = p.fst ∧ j = p.snd ↔ p = (i, j)
[PROOFSTEP]
aesop
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i j : n
x : A
t : ∀ (p : n × n), i = p.fst ∧ j = p.snd ↔ p = (i, j)
⊢ ↑(matrixEquivTensor R A n) (stdBasisMatrix i j x) = x ⊗ₜ[R] stdBasisMatrix i j 1
[PROOFSTEP]
simp [ite_tmul, t, stdBasisMatrix]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : A
M : Matrix n n R
⊢ ↑(AlgEquiv.symm (matrixEquivTensor R A n)) (a ⊗ₜ[R] M) = Matrix.map M fun x => a * ↑(algebraMap R A) x
[PROOFSTEP]
simp [matrixEquivTensor, MatrixEquivTensor.toFunAlgHom, algHomOfLinearMapTensorProduct, MatrixEquivTensor.toFunLinear]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : Fintype n
inst✝ : DecidableEq n
a : A
M : Matrix n n R
⊢ AddHom.toFun (lift (toFunBilinear R A n)).toAddHom (a ⊗ₜ[R] M) = Matrix.map M fun x => a * ↑(algebraMap R A) x
[PROOFSTEP]
rfl
