Documentation

Mathlib.LinearAlgebra.Eigenspace.Zero

Results on the eigenvalue 0 #

In this file we provide equivalent characterizations of properties related to the eigenvalue 0, such as being nilpotent, having determinant equal to 0, having a non-trivial kernel, etc...

Main results #

theorem LinearMap.charpoly_eq_X_pow_iff {R : Type u_1} {M : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] [IsNoetherian R M] (φ : Module.End R M) :
charpoly φ = Polynomial.X ^ Module.finrank R M ∀ (m : M), ∃ (n : ), (φ ^ n) m = 0