case a.a.h
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ coeff (↑matPolyEquiv (charmatrix M)) k i j = coeff (X - ↑C M) k i j
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ↑matPolyEquiv (charmatrix M) = X - ↑C M
ext (k i j)
case a.a.h
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ coeff (charmatrix M i j) k = (coeff X k - coeff (↑C M) k) i j
case a.a.h
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ coeff (↑matPolyEquiv (charmatrix M)) k i j = coeff (X - ↑C M) k i j
simp only [matPolyEquiv_coeff_apply, coeff_sub, Pi.sub_apply]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : i = j
⊢ coeff (charmatrix M i j) k = (coeff X k - coeff (↑C M) k) i j

case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ coeff (charmatrix M i j) k = (coeff X k - coeff (↑C M) k) i j
case a.a.h
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ coeff (charmatrix M i j) k = (coeff X k - coeff (↑C M) k) i j
by_cases h : i = j
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ coeff (charmatrix M i i) k = (coeff X k - coeff (↑C M) k) i i
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : i = j
⊢ coeff (charmatrix M i j) k = (coeff X k - coeff (↑C M) k) i j
subst h
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ coeff X k - coeff (↑C (M i i)) k = (coeff X k - coeff (↑C M) k) i i
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ coeff (charmatrix M i i) k = (coeff X k - coeff (↑C M) k) i i
rw [charmatrix_apply_eq, coeff_sub]
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i i
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ coeff X k - coeff (↑C (M i i)) k = (coeff X k - coeff (↑C M) k) i i
simp only [coeff_X, coeff_C]
no goals
case pos
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
⊢ ((if 1 = k then 1 else 0) - if k = 0 then M i i else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i i
split_ifs <;> simp
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-if k = 0 then M i j else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i j
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ coeff (charmatrix M i j) k = (coeff X k - coeff (↑C M) k) i j
rw [charmatrix_apply_ne _ _ _ h, coeff_X, coeff_neg, coeff_C, coeff_C]
no goals
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-if k = 0 then M i j else 0) = ((if 1 = k then 1 else 0) - if k = 0 then M else 0) i j
split_ifs <;> simp [h]