English
Let M be a Coxeter matrix on B. The set of Coxeter relations associated to M consists of all words in the free group on B obtained by applying the matrix to each pair of indices; equivalently, relationsSet(M) = { M.relation(i,j) | i,j ∈ B }.
Русский
Пусть M — матрица Коксетера на произвольном множестве B. Множество отношений Коксетера, ассоциированное с M, состоит из всех слов в свободной группе на B, полученных применением к каждому диапазону пары индексов соответствующего отношения; эквивалентно relationsSet(M) = { M.relation(i, j) | i,j ∈ B }.
LaTeX
$$$\operatorname{relationsSet}(M) = \{\, M.\operatorname{relation}(i,j) \mid i,j \in B \ \}$$$
Lean4
/-- The set of all Coxeter relations associated to the Coxeter matrix $M$. -/
def relationsSet : Set (FreeGroup B) :=
range <| uncurry M.relation
