root' — Mathlib

English

For each i, the root i is viewed as a linear functional on the weight space N, denoted root'(i) ∈ N^*.

Русский

Для каждого i корень i рассматривается как линейный функционал на весовом пространстве N, тождественно root'(i) ∈ N^*.

LaTeX

$$$ root'(i) \in N^* $$$

Lean4

/-- Roots written as functionals on the coweight space. -/
abbrev root' (i : ι) : Dual R N :=
  P.toLinearMap (P.root i)

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