English
Any property that holds for the identity, is preserved by generators, inverses, and products, holds for every element of the free group.
Русский
Любое свойство, содержащееся для единицы и сохраняющееся при применения генераторов, обратных и умножения, выполняется для каждого элемента свободной группы.
LaTeX
$$$\\forall C:\\ FreeGroup(\\alpha) \\to \\text{Prop},\\ C(1) \\land (\\forall x, C( FreeGroup.of(x))) \\land (\\forall x, C( FreeGroup.of(x)) \\to C((FreeGroup.of(x))^{-1})) \\land (\\forall x,y, C(x) \\to C(y) \\to C(x*y)) \\Rightarrow \\forall z, C(z)$$$
Lean4
/-- `of` is the canonical injection from the type to the free group over that type by sending each
element to the equivalence class of the letter that is the element. -/
@[to_additive /-- `of` is the canonical injection from the type to the free group over that type
by sending each element to the equivalence class of the letter that is the element. -/
]
def of (x : α) : FreeGroup α :=
mk [(x, true)]
