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
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
have t : ∀ p : n × n, i = p.1 ∧ j = p.2 ↔ p = (i, j) := by aesop
no goals
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
simp [ite_tmul, t, stdBasisMatrix]
no goals
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)
aesop