English
There is a canonical membership relation on M×M to Con M given by (a,b) ∈ M×M iff c a b.
Русский
Существует каноническое отношение принадлежности на M×M в Con M: (a,b) относится к c тогда, когда c a b.
LaTeX
$$$\\text{Membership} (M\\times M)\\; (Con\\; M)\\;:\\; (a,b) \\in M\\times M \\iff c\\ a\\ b$$$
Lean4
/-- Given a type `M` with a multiplication, a congruence relation `c` on `M`, and elements of `M`
`x, y`, `(x, y) ∈ M × M` iff `x` is related to `y` by `c`. -/
@[to_additive instMembershipProd /-- Given a type `M` with an addition, `x, y ∈ M`, and an additive congruence relation
`c` on `M`, `(x, y) ∈ M × M` iff `x` is related to `y` by `c`. -/
]
instance instMembershipProd : Membership (M × M) (Con M) :=
⟨fun c x => c x.1 x.2⟩
