Theorems · Theorem · linear algebra

LinearMap.charpoly_constantCoeff_eq_zero_iff

∀ {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),
  Polynomial.constantCoeff (LinearMap.charpoly φ) = 0 ↔ ∃ m, m ≠ 0 ∧ φ m = 0

Defined in

Mathlib.LinearAlgebra.Eigenspace.Zero

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleModule.Finite