rootSystem_pairing_apply

Mathlib.Algebra.Lie.Weights.RootSystem

URI: https://scilib.ai/kg/mathlib#LieAlgebra.IsKilling.rootSystem_pairing_apply

English

The pairing on the root system is given by the evaluation of a weight on a coroot: ⟨β,α⟩ = β(α∨).

Русский

Паринг корневой системы задаётся оценкой веса на короу: ⟨β,α⟩ = β(α∨).

LaTeX

$$$(\text{rootSystem}(H)).pairing(β, α) = β(\operatorname{coroot}(α))$$$

Lean4

@[simp]
theorem rootSystem_pairing_apply (α β) : (rootSystem H).pairing β α = β.1 (coroot α.1) :=
  rfl

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

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

Разделы

Аффилиация

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