injOn_genEigenspace — Mathlib

English

The map μ ↦ genEigenspace(f, μ, k) is injective on the domain where genEigenspace is nontrivial.

Русский

Отображение μ → genEigenspace(f, μ, k) инъективно на области, где пространство ненулевое.

LaTeX

$$$\\text{InjOn}\\bigl(\\lambda \\mu,\\; f.genEigenspace(\\mu, k)\\bigr)\\;\\{\\mu : R \\mid f.genEigenspace(\\mu, k) \\neq \\{0\\}\\}.$$$

Lean4

theorem injOn_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) :
    InjOn (f.genEigenspace · k) {μ | f.genEigenspace μ k ≠ ⊥} :=
  by
  rintro μ₁ _ μ₂ hμ₂ hμ₁₂
  by_contra contra
  apply hμ₂
  simpa only [hμ₁₂, disjoint_self] using f.disjoint_genEigenspace contra k k

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