English
A torsion monoid can be equipped with a group structure by defining inverse as g^(order(g)-1).
Русский
Торсионный моноид можно наделить структурой группы, задав обратный элемент через g^(order(g)-1).
LaTeX
$$$\exists$ Group structure on G with inv(g) = g^{\operatorname{order}(g)-1}$ and the given monoid operations.$$
Lean4
/-- Torsion monoids are really groups. -/
@[to_additive /-- Torsion additive monoids are really additive groups -/
]
noncomputable def group [Monoid G] (tG : IsTorsion G) : Group G :=
{ ‹Monoid G› with
inv := fun g => g ^ (orderOf g - 1)
inv_mul_cancel := fun g => by
rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]
exact (tG g).orderOf_pos }
