eigenspaces_iSupIndep — Mathlib

English

The eigenspaces of a linear operator form an independent family of subspaces of M.

Русский

Собственные подпространства линейного оператора образуют независимое семейство подпространств M.

LaTeX

$$$iSupIndep\\, f.eigenspace$$$

Lean4

/-- The eigenspaces of a linear operator form an independent family of subspaces of `M`.  That is,
any eigenspace has trivial intersection with the span of all the other eigenspaces. -/
theorem eigenspaces_iSupIndep [NoZeroSMulDivisors R M] (f : End R M) : iSupIndep f.eigenspace :=
  (f.independent_genEigenspace 1).mono fun _ ↦ le_rfl

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