root'_coroot_eq_pairing

Mathlib.LinearAlgebra.RootSystem.Defs

URI: https://scilib.ai/kg/mathlib#RootPairing.root'_coroot_eq_pairing

English

root' i applied to coroot j equals the pairing: root'(i)(coroot(j)) = pairing(i,j).

Русский

root'(i) применяемый к coroot(j) даёт парирование: root'(i)(coroot(j)) = pairing(i,j).

LaTeX

$$$ root'(i)(coroot(j)) = pairing(i,j) $$$

Lean4

@[simp]
theorem root'_coroot_eq_pairing : P.root' i (P.coroot j) = P.pairing i j :=
  rfl

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

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

Разделы

Аффилиация

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