English
There is an induction principle for the presented group: to prove a property for all elements, it suffices to prove it for canonical representatives from generators and extend via the quotient construction.
Русский
Для представленной группы существует принцип индукции: чтобы доказать свойство для всех элементов, достаточно доказать его для канонических представителей генерируемых элементов и распространить через факторную конструкцию.
LaTeX
$$Induction on $\mathrm{PresentedGroup}(\mathrm{rels})$ via $\mathrm{mk}$: for any property $C$, if $C(\mathrm{mk}_{\mathrm{rels}}(z))$ holds for all free group words $z$, then $C$ holds for all elements.$$
Lean4
@[induction_eliminator]
theorem induction_on {rels : Set (FreeGroup α)} {C : PresentedGroup rels → Prop} (x : PresentedGroup rels)
(H : ∀ z, C (mk rels z)) : C x :=
Quotient.inductionOn' x H
