injOn_maxGenEigenspace — Mathlib

English

The map μ ↦ maxGenEigenspace(f, μ) is injective on the domain where maxGenEigenspace μ ≠ ⊥.

Русский

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

LaTeX

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

Lean4

theorem injOn_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) :
    InjOn (f.maxGenEigenspace ·) {μ | f.maxGenEigenspace μ ≠ ⊥} :=
  injOn_genEigenspace f ⊤

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