chainLength_neg — Mathlib

English

For α nonzero, the root space at n • α + β is nontrivial exactly when n lies in the interval determined by chainTop and chainBot coefficients: n ∈ [−chainBotCoeff α β, chainTopCoeff α β].

Русский

Для α ≠ 0 пространство корня при n • α + β тривиально тогда и только тогда, когда n лежит в интервале, задаваемом chainTop и chainBotCoeff.

LaTeX

$$$\text{rootSpace}(H, n \cdot α + β) \neq ⊥ \;\iff\; n \in \mathop{\mathrm{Icc}}(-\operatorname{chainBotCoeff}(α, β), \operatorname{chainTopCoeff}(α, β))$$$

Lean4

@[simp]
theorem chainLength_neg : chainLength (-α) β = chainLength α β := by
  rw [← chainBotCoeff_add_chainTopCoeff, ← chainBotCoeff_add_chainTopCoeff, add_comm, Weight.coe_neg, chainTopCoeff_neg,
    chainBotCoeff_neg]

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