genWeightSpace_ne_bot — Mathlib

English

A simp lemma clarifies the equality of a maximal generalized eigenspace under various equivalent formulations; essentially a simplification of maxGenEigenspace equality conditions.

Русский

Лемма упрощения объясняет равенство максимального обобщенного собственного пространства при эквивалентных формулировках; упрощает условия равенства maxGenEigenspace.

LaTeX

$$$ (f)^{k} m = 0 \\;\\text{ equivalent forms}$$$

Lean4

theorem genWeightSpace_ne_bot (χ : Weight R L M) : genWeightSpace M χ ≠ ⊥ :=
  χ.genWeightSpace_ne_bot'

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