hasUnifEigenvalue_iff_hasUnifEigenvalue_one

English

For a linear endomorphism f, μ ∈ R, and k > 0, f HasUnifEigenvalue μ k iff f HasUnifEigenvalue μ 1 (i.e., generalized eigenvalues for positive exponent reduce to ordinary eigenvalues).

Русский

Для линейного эндоморфа f и скаляра μ ∈ R верно: μ является обобщённым собственным значением для любого положительного показателя k тогда и только тогда, когда μ является собственным значением f (показатель 1).

LaTeX

$$$\forall f: \mathrm{End}_R M,\; \mu \in R,\; k: \mathbb{N}_>0:\; f\text{ HasUnifEigenvalue } \mu k \iff f\text{ HasUnifEigenvalue } \mu 1$$$

Lean4

/-- Generalized eigenvalues are actually just eigenvalues. -/
@[simp]
theorem hasUnifEigenvalue_iff_hasUnifEigenvalue_one {f : End R M} {μ : R} {k : ℕ∞} (hk : 0 < k) :
    f.HasUnifEigenvalue μ k ↔ f.HasUnifEigenvalue μ 1 :=
  ⟨HasUnifEigenvalue.lt zero_lt_one, HasUnifEigenvalue.lt hk⟩

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