chainBot — Mathlib

English

The first weight in the α-chain through β is the weight χ_bot with value (−chainBotCoeff α β)·α + β and nontrivial weight space.

Русский

Первый вес в α-цепочке через β — это вес χ_bot со значением (−chainBotCoeff α β)·α + β и ненулевым весовым пространством.

LaTeX

$$$ \\text{chainBot}(α, β) = ((-\\text{chainBotCoeff}(α, β)) \\cdot α + β,\\; genWeightSpace M((-\\text{chainBotCoeff}(α, β)) \\cdot α + β) ≠ ⊥) $$$

Lean4

/-- The first weight in an `α`-chain through `β`. -/
noncomputable def chainBot (α : L → R) (β : Weight R L M) : Weight R L M :=
  ⟨(-chainBotCoeff α β : ℤ) • α + β, genWeightSpace_neg_zsmul_add_ne_bot α β le_rfl⟩

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