English
An element a of a monoid is a unit if and only if there exists a unit u with (u : M) = a.
Русский
Элемент a моноида является единицей тогда и только тогда, когда существует единица u такая, что (u : M) = a.
LaTeX
$$$\IsUnit(a) \iff \exists u : M^{\times}, (u : M) = a$$$
Lean4
/-- An element `a : M` of a `Monoid` is a unit if it has a two-sided inverse.
The actual definition says that `a` is equal to some `u : Mˣ`, where
`Mˣ` is a bundled version of `IsUnit`. -/
@[to_additive /-- An element `a : M` of an `AddMonoid` is an `AddUnit` if it has a two-sided
additive inverse. The actual definition says that `a` is equal to some `u : AddUnits M`,
where `AddUnits M` is a bundled version of `IsAddUnit`. -/
]
def IsUnit [Monoid M] (a : M) : Prop :=
∃ u : Mˣ, (u : M) = a
