coxeterWeight_swap

Mathlib.LinearAlgebra.RootSystem.Defs

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

English

The Coxeter weight is symmetric: coxeterWeight i j = coxeterWeight j i.

Русский

Вес Коцитора симметричен: coxeterWeight i j = coxeterWeight j i.

LaTeX

$$$$ \\mathrm{coxeterWeight}(i,j) = \\mathrm{coxeterWeight}(j,i). $$$$

Lean4

theorem coxeterWeight_swap : coxeterWeight P i j = coxeterWeight P j i := by simp only [coxeterWeight, mul_comm]

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

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

Разделы

Аффилиация

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