genWeightSpace_neg_zsmul_add_ne_bot

English

The zsmul (integer scalar) version of the top coefficient yields a nontrivial weight space at (n+1) · α + β when n = chainTopCoeff α β.

Русский

Целочисленное умножение версии верхнего коэффициента даёт ненулевое весовое пространство для (n+1) · α + β при n = chainTopCoeff α β.

LaTeX

$$$ genWeightSpace M \\big((\\text{chainTopCoeff}(α, β) + 1) \\cdot α + β\\big) \\neq ⊥ $$$

Lean4

theorem genWeightSpace_neg_zsmul_add_ne_bot {n : ℕ} (hn : n ≤ chainBotCoeff α β) :
    genWeightSpace M ((-n : ℤ) • α + β : L → R) ≠ ⊥ := by apply genWeightSpace_zsmul_add_ne_bot α β <;> omega

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