finite_genWeightSpace_ne_bot — Mathlib

English

A refined version showing finiteness of the set {χ | genWeightSpace M χ ≠ ⊥} under hypotheses.

Русский

Уточнение: конечность множества χ, для которых весовое пространство непусто, при заданных гипотезах.

LaTeX

$$$\{\chi : L \to R \mid genWeightSpace M χ \neq ⊥\}.Finite$$$

Lean4

theorem finite_genWeightSpace_ne_bot [NoZeroSMulDivisors R M] [IsNoetherian R M] :
    {χ : L → R | genWeightSpace M χ ≠ ⊥}.Finite :=
  WellFoundedGT.finite_ne_bot_of_iSupIndep (iSupIndep_genWeightSpace R L M)

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