pairing_same

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

For any i, the pairing of i with itself equals 2: pairing(i,i) = 2.

Русский

Для любого i парирование с самим собой равно 2: pairing(i,i) = 2.

LaTeX

$$$ \mathrm{pairing}(i,i) = 2 $$$

Lean4

@[simp]
theorem pairing_same : P.pairing i i = 2 :=
  P.root_coroot_two i

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

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

Разделы

Аффилиация

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