iSupIndep_genWeightSpace' — Mathlib

English

A variant of independence for weight spaces parameterized through Weight set.

Русский

Вариант независимости весовых пространств, параметризованный через множество весов.

LaTeX

$$iSupIndep (fun χ => genWeightSpace M χ)^{'}$$

Lean4

theorem iSupIndep_genWeightSpace' [NoZeroSMulDivisors R M] : iSupIndep fun χ : Weight R L M ↦ genWeightSpace M χ :=
  (iSupIndep_genWeightSpace R L M).comp <| Subtype.val_injective.comp (Weight.equivSetOf R L M).injective

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