toWeightBasis — Mathlib

English

The i-th element of the weight basis equals the root P.root i; equivalently, the weight-basis coefficients match the root values.

Русский

i-й элемент веса-базиса равен корню P.root i; коэффициенты базиса веса совпадают с корнями.

LaTeX

$$b.toWeightBasis i = P.root i$$

Lean4

/-- A base of a root system yields a basis of the root space. -/
def toWeightBasis : Basis b.support R M :=
  Basis.mk b.linearIndepOn_root <|
    by
    change ⊤ ≤ span R (range <| P.root ∘ ((↑) : b.support → ι))
    simp [range_comp]

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