Theorems · Theorem · linear algebra

LinearMap.hasEigenvalue_zero_tfae

∀ {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [inst_3 : Module.Finite K M] (φ : Module.End K M),
  [φ.HasEigenvalue 0, (minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) = 0, LinearMap.det φ = 0,
      ⊥ < LinearMap.ker φ, ∃ m, m ≠ 0 ∧ φ m = 0].TFAE

Defined in

Mathlib.LinearAlgebra.Eigenspace.Zero

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleModule.Finite