English
If every element of a monoid M is a unit, then M can be equipped with a group structure, where the inverse of an element a is the unit inverse of a, i.e., a^{-1} corresponds to ↑((h a).unit)^{-1}.
Русский
Если каждый элемент моноида M является единицей, то M можно наделить групповой структурой, где обратное элемента a равно единице соответствующей единице a, то есть a^{-1} соответствует ↑((h a).unit)^{-1}.
LaTeX
$$$\\exists \\text{group structure on } M\\text{ such that } a^{-1} = \\uparrow\\big( (h(a)).unit \\big)^{-1} \\quad (\\forall a \\in M)$$$
Lean4
/-- Constructs a `Group` structure on a `Monoid` consisting only of units. -/
noncomputable def groupOfIsUnit [hM : Monoid M] (h : ∀ a : M, IsUnit a) : Group M :=
{ hM with toInv := invOfIsUnit h,
inv_mul_cancel := fun a => by
change ↑(h a).unit⁻¹ * a = 1
rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one] }
