R : Type u_1
A : Type ?u.570514
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
⊢ coeff (↑(AlgEquiv.symm matPolyEquiv) p i j) k = coeff p k i j
R : Type u_1
A : Type ?u.570514
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ coeff (↑(AlgEquiv.symm matPolyEquiv) p i j) k = coeff p k i j
have t : p = matPolyEquiv (matPolyEquiv.symm p) := by simp
R : Type u_1
A : Type ?u.570514
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
⊢ coeff (↑(AlgEquiv.symm matPolyEquiv) p i j) k = coeff (↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)) k i j
R : Type u_1
A : Type ?u.570514
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
⊢ coeff (↑(AlgEquiv.symm matPolyEquiv) p i j) k = coeff p k i j
conv_rhs => rw [t]
no goals
R : Type u_1
A : Type ?u.570514
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
⊢ coeff (↑(AlgEquiv.symm matPolyEquiv) p i j) k = coeff (↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)) k i j
simp only [matPolyEquiv_coeff_apply]
no goals
R : Type u_1
A : Type ?u.570514
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
simp