English
The submonoid of M × M corresponding to a congruence c on M is the set { (x,y) | x c y }. This realizes the coerced submonoid c.submonoid.
Русский
Подмоноид M × M, соответствующий конгруэнции c на M, состоит из пар { (x,y) | x c y }. Это и есть сопряжённый подмонуид c.submonoid.
LaTeX
$$Con.submonoid is the Submonoid with carrier = {x | c x.1 x.2}$$
Lean4
/-- Coercion from a congruence relation `c` on a monoid `M` to the submonoid of `M × M` whose
elements are `(x, y)` such that `x` is related to `y` by `c`. -/
@[to_additive /-- Coercion from a congruence relation `c` on an `AddMonoid` `M`
to the `AddSubmonoid` of `M × M` whose elements are `(x, y)` such that `x`
is related to `y` by `c`. -/
]
instance toSubmonoid : Coe (Con M) (Submonoid (M × M)) :=
⟨fun c => c.submonoid⟩
