genWeightSpace_chainBotCoeff_sub_one_zsmul_sub

English

The weight with coefficient (−chainBotCoeff α β − 1) in front of α, plus β, yields a trivial weight space.

Русский

Вес с коэффициентом (−chainBotCoeff α β − 1) перед α плюс β даёт тривиальное весовое пространство.

LaTeX

$$$ genWeightSpace M \\big( (-(\\text{chainBotCoeff}(\\alpha, \\beta)) - 1) \\cdot \\alpha + \\beta \\big) = \\bot $$$

Lean4

theorem genWeightSpace_chainBotCoeff_sub_one_zsmul_sub :
    genWeightSpace M ((-chainBotCoeff α β - 1 : ℤ) • α + β : L → R) = ⊥ := by
  rw [sub_eq_add_neg, ← neg_add, neg_smul, ← smul_neg, chainBotCoeff,
    genWeightSpace_chainTopCoeff_add_one_zsmul_add _ _ (by simpa using hα)]

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