English
The free group FreeGroup α is equipped with a canonical group structure with multiplication given by concatenation of representatives, identity, and inverse defined in the standard way.
Русский
Свободная группа FreeGroup α оснащена естественной структурой группы: произведение задано конкатенацией слов, единица — пустое слово, обратное — обычное обратное слово.
LaTeX
$$$\\text{FreeGroup}(\\alpha)$ is a group with $x*y$ defined by concatenation of words, identity $1$, and inverse $x^{-1}$ given by invRev.$$
Lean4
@[to_additive]
instance : Group (FreeGroup α) where
mul := (· * ·)
one := 1
inv := Inv.inv
mul_assoc := by rintro ⟨L₁⟩ ⟨L₂⟩ ⟨L₃⟩; simp
one_mul := by rintro ⟨L⟩; rfl
mul_one := by rintro ⟨L⟩; simp [one_eq_mk]
inv_mul_cancel := by
rintro ⟨L⟩
exact List.recOn L rfl fun ⟨x, b⟩ tl ih => Eq.trans (Quot.sound <| by simp [invRev]) ih
