toCoweightBasis — Mathlib

English

A base of a root system yields a basis of the coroot space; the coweight basis is the corresponding dual notion, obtained by flipping the root system.

Русский

База корневой системы порождает базис пространства коротов; базис ковоится является двойственной аналогией через разворот корневой системы.

LaTeX

$$toCoweightBasis : Basis b.support R N$$

Lean4

/-- A base of a root system yields a basis of the coroot space. -/
def toCoweightBasis : Basis b.support R N :=
  Base.toWeightBasis (P := P.flip) b.flip

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