coe_chainBot — Mathlib

English

Adding α to the chainTop weight yields a bottom weight space, under the nonzero α assumption.

Русский

При условии ненулевого α добавление α к верхнему весу приводит к тривиальному весовому пространству.

LaTeX

$$$ genWeightSpace\\ M( α + \\text{chainTop}(α, β) ) = ⊥ \\quad\\text{for } α \\neq 0 $$$

Lean4

@[simp]
theorem coe_chainBot : (chainBot α β : L → R) = (-chainBotCoeff α β : ℤ) • α + β :=
  rfl

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