charpoly_constantCoeff_eq_zero_iff

English

The constant term of the charpoly is zero if and only if there exists a nonzero vector m with φ m = 0.

Русский

Постоянный член характеристической полиномии равен нулю тогда и только тогда, когда существует ненулевой вектор m с φ m = 0.

LaTeX

$$constantCoeff φ.charpoly = 0 ↔ ∃ m ≠ 0, φ m = 0$$

Lean4

theorem charpoly_constantCoeff_eq_zero_iff (φ : Module.End K M) :
    constantCoeff φ.charpoly = 0 ↔ ∃ (m : M), m ≠ 0 ∧ φ m = 0 :=
  (hasEigenvalue_zero_tfae φ).out 2 5

Похожие утверждения