Theorems · Theorem · linear algebra

LinearMap.not_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), φ m = 0 → m = 0].TFAE

Defined in

Mathlib.LinearAlgebra.Eigenspace.Zero

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleModule.Finite