R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ ↑(AlgEquiv.symm (polyEquivTensor R (Matrix n n R)))
      (↑(Algebra.TensorProduct.comm R R[X] (Matrix n n R)) (↑(monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1)) =
    ↑(monomial k) (stdBasisMatrix i j x)
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ ↑matPolyEquiv (stdBasisMatrix i j (↑(monomial k) x)) = ↑(monomial k) (stdBasisMatrix i j x)
simp only [matPolyEquiv, AlgEquiv.trans_apply, matrixEquivTensor_apply_std_basis]
case a
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ ↑(polyEquivTensor R (Matrix n n R))
      (↑(AlgEquiv.symm (polyEquivTensor R (Matrix n n R)))
        (↑(Algebra.TensorProduct.comm R R[X] (Matrix n n R)) (↑(monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1))) =
    ↑(polyEquivTensor R (Matrix n n R)) (↑(monomial k) (stdBasisMatrix i j x))
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ ↑(AlgEquiv.symm (polyEquivTensor R (Matrix n n R)))
      (↑(Algebra.TensorProduct.comm R R[X] (Matrix n n R)) (↑(monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1)) =
    ↑(monomial k) (stdBasisMatrix i j x)
apply (polyEquivTensor R (Matrix n n R)).injective
case a
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] ↑(monomial k) x = ↑↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] X ^ k
case a
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ ↑(polyEquivTensor R (Matrix n n R))
      (↑(AlgEquiv.symm (polyEquivTensor R (Matrix n n R)))
        (↑(Algebra.TensorProduct.comm R R[X] (Matrix n n R)) (↑(monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1))) =
    ↑(polyEquivTensor R (Matrix n n R)) (↑(monomial k) (stdBasisMatrix i j x))
simp only [AlgEquiv.apply_symm_apply,Algebra.TensorProduct.comm_tmul,
  polyEquivTensor_apply, eval₂_monomial]
case a
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] ↑(monomial k) x = ↑↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)
case a
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] ↑(monomial k) x = ↑↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] X ^ k
simp only [Algebra.TensorProduct.tmul_mul_tmul, one_pow, one_mul, Matrix.mul_one,
  Algebra.TensorProduct.tmul_pow, Algebra.TensorProduct.includeLeft_apply, mul_eq_mul]
case a
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (x • stdBasisMatrix i j 1) ⊗ₜ[R] (X ^ k) = ↑↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)
case a
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] ↑(monomial k) x = ↑↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)
rw [← smul_X_eq_monomial, ← TensorProduct.smul_tmul]
no goals
case a
R : Type u_1
A : Type ?u.483263
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (x • stdBasisMatrix i j 1) ⊗ₜ[R] (X ^ k) = ↑↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)
congr with i' <;> simp [stdBasisMatrix]