coroot_root_eq_pairing

Mathlib.LinearAlgebra.RootSystem.Defs

URI: https://scilib.ai/kg/mathlib#RootPairing.coroot_root_eq_pairing

English

If P.root k = P.root i + P.root j, then P.pairing k l = P.pairing i l + P.pairing j l.

Русский

Если P.root k = P.root i + P.root j, то P.pairing k l = P.pairing i l + P.pairing j l.

LaTeX

$$$ \text{If } P.root(k) = P.root(i) + P.root(j), \; P.pairing(k,l) = P.pairing(i,l) + P.pairing(j,l) $$$

Lean4

theorem coroot_root_eq_pairing : P.toLinearMap.flip (P.coroot i) (P.root j) = P.pairing j i := by simp

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

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

Разделы

Аффилиация

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