English
On a monoid M, define x ~ y iff there exists a unit u with x u = y; this defines a Setoid on M whose equivalence is given by Associated.refl, Associated.symm, and Associated.trans.
Русский
На моноиде M задаём x ~ y тогда и только тогда, когда существует единица u такая, что x u = y; это задаёт множество эквивалентности на M, эквивалентность задаётся refl, symm, trans.
LaTeX
$$$\\text{Associated.setoid}(M) : Setoid\, M\\text{ with } r(x,y) \\Leftrightarrow \\text{Associated } x y$, equivalence given by refl, symm, trans.$$
Lean4
/-- The setoid of the relation `x ~ᵤ y` iff there is a unit `u` such that `x * u = y` -/
protected def setoid (M : Type*) [Monoid M] : Setoid M
where
r := Associated
iseqv := ⟨Associated.refl, Associated.symm, Associated.trans⟩
