exp_ne_zero — Mathlib

English

The exponent k of a uniform eigenvalue cannot be zero: if HasUnifEigenvalue f μ k, then k ≠ 0.

Русский

Показатель k унифицированного собственного значения не может быть равен нулю: если HasUnifEigenvalue f μ k, то k ≠ 0.

LaTeX

$$exp_ne_zero {f} {μ} {k} (h : f.HasUnifEigenvalue μ k) : k ≠ 0$$

Lean4

/-- The exponent of a generalized eigenvalue is never 0. -/
theorem exp_ne_zero {f : End R M} {μ : R} {k : ℕ} (h : f.HasUnifEigenvalue μ k) : k ≠ 0 :=
  by
  rintro rfl
  simp [HasUnifEigenvalue, Nat.cast_zero, genEigenspace_zero] at h

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