exp_ne_zero_of_hasGenEigenvalue — Mathlib

English

If f has a generalized eigenvalue μ of rank k, then k ≠ 0.

Русский

Если у f есть обобщённое эйгензначение μ ранга k, то k не равно нулю.

LaTeX

$$$\\text{If } f.HasGenEigenvalue\\;\\mu\\;k, \\;\\ k \\neq 0.$$$

Lean4

/-- The exponent of a generalized eigenvalue is never 0. -/
theorem exp_ne_zero_of_hasGenEigenvalue {f : End R M} {μ : R} {k : ℕ} (h : f.HasGenEigenvalue μ k) : k ≠ 0 :=
  HasUnifEigenvalue.exp_ne_zero h

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