English
The negation of the eigenvalue 0 conditions is equivalent to the negation of other spectral conditions: there is no eigenvalue 0, minpoly 0 is not a root, etc.
Русский
Утверждение о том, что 0 не является спектральным значением, эквивалентно отрицаниям прочих спектральных условий.
LaTeX
$$¬HasEigenvalue φ 0, ¬IsRoot (minpoly K φ) 0, φ.charpoly ≠ 0, det φ ≠ 0, ker φ = ⊥, ∀ m, φ m = 0 → m = 0$$
Lean4
theorem not_hasEigenvalue_zero_tfae (φ : Module.End K M) :
List.TFAE
[¬Module.End.HasEigenvalue φ 0, ¬IsRoot (minpoly K φ) 0, constantCoeff φ.charpoly ≠ 0, LinearMap.det φ ≠ 0,
ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0] :=
by
have := (hasEigenvalue_zero_tfae φ).not
dsimp only [List.map] at this
push_neg at this
have aux₁ : ∀ m, (m ≠ 0 → φ m ≠ 0) ↔ (φ m = 0 → m = 0) := by intro m; apply not_imp_not
have aux₂ : ker φ = ⊥ ↔ ¬⊥ < ker φ := by rw [bot_lt_iff_ne_bot, not_not]
simpa only [aux₁, aux₂] using this
