instGroupGroup — Mathlib

English

The Coxeter group associated to M, denoted M.Group, carries a group structure; concretely, it is the quotient of the free group on B by the normal closure of M.relationsSet.

Русский

Группа Коксетера, связанная с M, образована как фактор-группа свободной группы на B по нормальному замыканию множества отношений M.relationsSet.

LaTeX

$$$M\text{.Group} \cong F(B) / \langle\!\langle \operatorname{relationsSet}(M) \rangle\!\rangle$$$

Lean4

instance : Group M.Group :=
  QuotientGroup.Quotient.group _

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