[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i : n
⊢ charmatrix M i i = X - ↑C (M i i)
[PROOFSTEP]
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply_eq, map_apply]
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
h : i ≠ j
⊢ charmatrix M i j = -↑C (M i j)
[PROOFSTEP]
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply_ne _ _ _ h, map_apply, sub_eq_neg_self]
[GOAL]
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
[PROOFSTEP]
ext k i j
[GOAL]
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
[PROOFSTEP]
simp only [matPolyEquiv_coeff_apply, coeff_sub, Pi.sub_apply]
[GOAL]
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
[PROOFSTEP]
by_cases h : i = j
[GOAL]
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
[PROOFSTEP]
subst h
[GOAL]
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
[PROOFSTEP]
rw [charmatrix_apply_eq, coeff_sub]
[GOAL]
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
[PROOFSTEP]
simp only [coeff_X, coeff_C]
[GOAL]
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
[PROOFSTEP]
split_ifs
[GOAL]
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
h✝¹ : 1 = k
h✝ : k = 0
⊢ 1 - M i i = (1 - M) i i
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : 1 = k
h✝ : ¬k = 0
⊢ 1 - 0 = (1 - 0) i i
[PROOFSTEP]
simp
[GOAL]
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
h✝¹ : ¬1 = k
h✝ : k = 0
⊢ 0 - M i i = (0 - M) i i
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i : n
h✝¹ : ¬1 = k
h✝ : ¬k = 0
⊢ 0 - 0 = (0 - 0) i i
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
rw [charmatrix_apply_ne _ _ _ h, coeff_X, coeff_neg, coeff_C, coeff_C]
[GOAL]
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
[PROOFSTEP]
split_ifs
[GOAL]
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
h✝¹ : k = 0
h✝ : 1 = k
⊢ -M i j = (1 - M) i j
[PROOFSTEP]
simp [h]
[GOAL]
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
h✝¹ : k = 0
h✝ : ¬1 = k
⊢ -M i j = (0 - M) i j
[PROOFSTEP]
simp [h]
[GOAL]
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
h✝¹ : ¬k = 0
h✝ : 1 = k
⊢ -0 = (1 - 0) i j
[PROOFSTEP]
simp [h]
[GOAL]
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
h✝¹ : ¬k = 0
h✝ : ¬1 = k
⊢ -0 = (0 - 0) i j
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
⊢ charmatrix (↑(reindex e e) M) = ↑(reindex e e) (charmatrix M)
[PROOFSTEP]
ext i j x
[GOAL]
case a.h.a
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
case neg
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : ¬i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
[PROOFSTEP]
all_goals simp [h]
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
i j : m
x : ℕ
h : ¬i = j
⊢ coeff (charmatrix (↑(reindex e e) M) i j) x = coeff (↑(reindex e e) (charmatrix M) i j) x
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
⊢ charpoly (↑(reindex e e) M) = charpoly M
[PROOFSTEP]
unfold Matrix.charpoly
[GOAL]
R : Type u
inst✝⁴ : CommRing R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type v
inst✝¹ : DecidableEq m
inst✝ : Fintype m
e : n ≃ m
M : Matrix n n R
⊢ det (charmatrix (↑(reindex e e) M)) = det (charmatrix M)
[PROOFSTEP]
rw [charmatrix_reindex, Matrix.det_reindex_self]
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
have h : M.charpoly • (1 : Matrix n n R[X]) = adjugate (charmatrix M) * charmatrix M := (adjugate_mul _).symm
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : charpoly M • 1 = adjugate (charmatrix M) * charmatrix M
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
apply_fun matPolyEquiv at h 
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : ↑matPolyEquiv (charpoly M • 1) = ↑matPolyEquiv (adjugate (charmatrix M) * charmatrix M)
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
simp only [matPolyEquiv.map_mul, matPolyEquiv_charmatrix] at h 
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : ↑matPolyEquiv (charpoly M • 1) = ↑matPolyEquiv (adjugate (charmatrix M)) * (X - ↑C M)
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
apply_fun fun p => p.eval M at h 
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (↑matPolyEquiv (charpoly M • 1)) = eval M (↑matPolyEquiv (adjugate (charmatrix M)) * (X - ↑C M))
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
rw [eval_mul_X_sub_C] at h 
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval M (↑matPolyEquiv (charpoly M • 1)) = 0
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
rw [matPolyEquiv_smul_one, eval_map] at h 
[GOAL]
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
h : eval₂ (algebraMap R (Matrix n n R)) M (charpoly M) = 0
⊢ ↑(aeval M) (charpoly M) = 0
[PROOFSTEP]
exact h
