relation

Mathlib.GroupTheory.Coxeter.Basic

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

Lean4

/-- The Coxeter relation associated to a Coxeter matrix $M$ and two indices $i, i' \in B$.
That is, the relation $(s_i s_{i'})^{M_{i, i'}}$, considered as an element of the free group
on $\{s_i\}_{i \in B}$.
If $M_{i, i'} = 0$, then this is the identity, indicating that there is no relation between
$s_i$ and $s_{i'}$. -/
def relation (i i' : B) : FreeGroup B :=
  (FreeGroup.of i * FreeGroup.of i') ^ M i i'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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