Theorems · Theorem · linear algebra

LinearMap.charpoly_nilpotent_tfae

∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.Finite R M] [inst_5 : Module.Free R M] [IsNoetherian R M] (φ : Module.End R M),
  [IsNilpotent φ, LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M, ∀ (m : M), ∃ n, (φ ^ n) m = 0,
      (LinearMap.charpoly φ).natTrailingDegree = Module.finrank R M].TFAE

Defined in

Mathlib.LinearAlgebra.Eigenspace.Zero

Cited by

2 results in Mathlib

Foundations

Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainAddCommGroupModuleModule.FiniteModule.FreeIsNoetherian