English
There is an induction principle for FreeGroup elements along their list representation: any property holding for the identity and closed under of/inv and multiplication holds for all group elements.
Русский
Существoвает принцип индукции для элементов FreeGroup по их списочной записи: свойство, выполняющееся для тождества и сохраняющееся под операций of/inv и умножения, выполняется для всех элементов группы.
LaTeX
$$$ \\forall z: FreeGroup\\,\\alpha, (C\\!:\\, FreeGroup\\alpha \\to \\Prop) \\, (C1) \\to (\\forall x, C(\\text{of } x)) \\, (\\forall x, C(\\mathrm{instInv}.inv(\\mathrm{of } x))) \\, (\\forall x y, C x \\to C y \\to C(x*y)) \\Rightarrow C z$$$
Lean4
@[to_additive (attr := elab_as_elim, induction_eliminator)]
protected theorem induction_on {C : FreeGroup α → Prop} (z : FreeGroup α) (C1 : C 1) (of : ∀ x, C <| of x)
(inv_of : ∀ x, C (.of x) → C (.of x)⁻¹) (mul : ∀ x y, C x → C y → C (x * y)) : C z :=
Quot.inductionOn z fun L ↦ L.recOn C1 fun ⟨x, b⟩ _tl ih ↦ b.recOn (mul _ _ (inv_of _ <| of x) ih) (mul _ _ (of x) ih)
