toCoweightBasis_apply

Mathlib.LinearAlgebra.RootSystem.Base

URI: https://scilib.ai/kg/mathlib#RootPairing.Base.toCoweightBasis_apply

English

The i-th element of the coweight basis equals the coroot P.coroot i.

Русский

i-й элемент базиса ковоевого пространства равен корооту P.coroot i.

LaTeX

$$b.toCoweightBasis i = P.coroot i$$

Lean4

@[simp]
theorem toCoweightBasis_apply (i : b.support) : b.toCoweightBasis i = P.coroot i :=
  b.flip.toWeightBasis_apply (P := P.flip) i

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru