case a.a.h
R : Type u_1
A : Type ?u.620220
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ coeff (↑matPolyEquiv (p • 1)) m i j = coeff (Polynomial.map (algebraMap R (Matrix n n R)) p) m i j
R : Type u_1
A : Type ?u.620220
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
⊢ ↑matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p
ext (m i j)
case a.a.h
R : Type u_1
A : Type ?u.620220
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ coeff ((p • 1) i j) m = if i = j then ↑(algebraMap R R) (coeff p m) else 0
case a.a.h
R : Type u_1
A : Type ?u.620220
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ coeff (↑matPolyEquiv (p • 1)) m i j = coeff (Polynomial.map (algebraMap R (Matrix n n R)) p) m i j
simp only [coeff_map, one_apply, algebraMap_matrix_apply, mul_boole, Pi.smul_apply,
  matPolyEquiv_coeff_apply]
no goals
case a.a.h
R : Type u_1
A : Type ?u.620220
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ coeff ((p • 1) i j) m = if i = j then ↑(algebraMap R R) (coeff p m) else 0
split_ifs <;> simp <;> rename_i h <;> simp [h]