English
If a monoid M has the property that every element is a unit, then one can define an inverse operation inv: M → M by inv(a) = ↑((h a).unit)^{-1}, where h(a) is the unit associated to a.
Русский
Пусть моноид M обладает свойством, что каждый элемент является единицей. Тогда задаётся обратная отображение inv: M → M по inv(a) = ↑((h(a)).unit)^{-1}, где h(a) — соответствующая единица.
LaTeX
$$$\\forall a \\in M,\\ inv(a) = \\uparrow\\big( (h(a)).unit \\big)^{-1}$$$
Lean4
/-- Constructs an inv operation for a `Monoid` consisting only of units. -/
noncomputable def invOfIsUnit [Monoid M] (h : ∀ a : M, IsUnit a) : Inv M where inv := fun a => ↑(h a).unit⁻¹
