R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(AlgEquiv.toLinearEquiv (algEquivMatrix (chooseBasis R M))) (↑(aeval f) (charpoly f)) = 0
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(aeval f) (charpoly f) = 0
apply (LinearEquiv.map_eq_zero_iff (algEquivMatrix (chooseBasis R M)).toLinearEquiv).1
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(aeval (↑↑(algEquivMatrix (chooseBasis R M)) f))
      (Matrix.charpoly (↑(toMatrix (chooseBasis R M) (chooseBasis R M)) f)) =
    0
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(AlgEquiv.toLinearEquiv (algEquivMatrix (chooseBasis R M))) (↑(aeval f) (charpoly f)) = 0
rw [AlgEquiv.toLinearEquiv_apply, ← AlgEquiv.coe_algHom, ← Polynomial.aeval_algHom_apply _ _ _,
  charpoly_def]
no goals
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] M
⊢ ↑(aeval (↑↑(algEquivMatrix (chooseBasis R M)) f))
      (Matrix.charpoly (↑(toMatrix (chooseBasis R M) (chooseBasis R M)) f)) =
    0
exact Matrix.aeval_self_charpoly _