chainLength_smul — Mathlib

English

Over a field of characteristic zero, for any x in the α-chain top root space, the scalar chainLength α β (viewed in the base field) acting on x yields the Lie bracket with the coroot α: (chainLength α β) · x = [coroot α, x].

Русский

В поле характеристика 0 для любого x из α-цепи в верхнем уровне корней действие скаляра chainLength α β на x равно скобке [coroot α, x].

LaTeX

$$$\big(\operatorname{chainLength}(\alpha, \beta)\big) \cdot x = [\operatorname{coroot}(\alpha), x]$$$

Lean4

theorem chainLength_smul {x} (hx : x ∈ rootSpace H (chainTop α β)) : (chainLength α β : K) • x = ⁅coroot α, x⁆ := by
  rw [Nat.cast_smul_eq_nsmul, chainLength_nsmul _ _ hx]

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