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
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
have h : M.charpoly • (1 : Matrix n n R[X]) = adjugate (charmatrix M) * charmatrix M :=
  (adjugate_mul _).symm
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
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
apply_fun matPolyEquiv  at h
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
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
simp only [matPolyEquiv.map_mul, matPolyEquiv_charmatrix] at h
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
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
apply_fun fun p => p.eval M  at h
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
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
rw [eval_mul_X_sub_C] at h
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
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
rw [matPolyEquiv_smul_one, eval_map] at h
no goals
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
exact h