symmetric

Mathlib.GroupTheory.Coxeter.Matrix

URI: https://scilib.ai/kg/mathlib#CoxeterMatrix.symmetric

English

The Coxeter matrix is symmetric: M(i,i') = M(i',i) for all i,i' in B.

Русский

Матрица Коксетера симметрична: M(i,i') = M(i',i) для всех i,i' ∈ B.

LaTeX

$$$$ M(i,i') = M(i',i) \\quad \\text{for all } i,i' \\in B. $$$$

Lean4

theorem symmetric (i i' : B) : M i i' = M i' i :=
  M.isSymm.apply i' i

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

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

Разделы

Аффилиация

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