exists_hasUnifEigenvector — Mathlib

English

If μ is a HasUnifEigenvalue μ k for f, there exists v with HasUnifEigenvector μ k v.

Русский

Если μ является HasUnifEigenvalue f μ k, существует вектор v, такой что HasUnifEigenvector f μ k v.

LaTeX

$$∀ {f μ k}, HasUnifEigenvalue f μ k → ∃ v, HasUnifEigenvector f μ k v$$

Lean4

theorem exists_hasUnifEigenvector {f : End R M} {μ : R} {k : ℕ∞} (hμ : f.HasUnifEigenvalue μ k) :
    ∃ v, f.HasUnifEigenvector μ k v :=
  Submodule.exists_mem_ne_zero_of_ne_bot hμ

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