English
Given a unit a, there is a corresponding unit element in the group of units, denoted aˣ, which maps to a in the monoid.
Русский
Дано единичное элемент a, существует соответствующий элемент группы единиц aˣ, который отображает a в моноиде.
LaTeX
$$$\forall a \in M^{\times}: \text{the corresponding unit in } M \text{ equals } a$$$
Lean4
/-- The element of the group of units, corresponding to an element of a monoid which is a unit. When
`α` is a `DivisionMonoid`, use `IsUnit.unit'` instead. -/
@[to_additive /-- The element of the additive group of additive units, corresponding to an element
of an additive monoid which is an additive unit. When `α` is a `SubtractionMonoid`, use
`IsAddUnit.addUnit'` instead. -/
]
protected noncomputable def unit (h : IsUnit a) : Mˣ :=
(Classical.choose h).copy a (Classical.choose_spec h).symm _ rfl
