independent_maxGenEigenspace — Mathlib

English

Let f be a linear endomorphism of a module M over a commutative ring R with NoZeroSmulDivisors. Then the family {f.maxGenEigenspace(μ) | μ ∈ R} is independent.

Русский

Пусть f — линейное отображение из M в себя над коммутативным кольцом R с условием NoZeroSmulDivisors. Тогда семейство {f.maxGenEigenspace(μ)} для μ ∈ R независимо.

LaTeX

$$$iSupIndep\\, f.maxGenEigenspace$$$

Lean4

theorem independent_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) : iSupIndep f.maxGenEigenspace := by
  apply independent_genEigenspace

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