English
Two elements are related by a congruence c iff they are equal in the quotient: a ≡_c b iff (a : c.Quotient) = (b : c.Quotient).
Русский
Два элемента связаны конгруэнцией c тогда и только тогда, когда они равны в факторе: a ≡_c b, если и только если a и b имеют одинаковый образ в факторе.
LaTeX
$$$(a : c.Quotient) = (b : c.Quotient) \\iff c\\ a\\ b$$$
Lean4
/-- Two elements are related by a congruence relation `c` iff they are represented by the same
element of the quotient by `c`. -/
@[to_additive (attr := simp) /-- Two elements are related by an additive congruence relation `c` iff
they are represented by the same element of the quotient by `c`. -/
]
protected theorem eq {a b : M} : (a : c.Quotient) = (b : c.Quotient) ↔ c a b :=
Quotient.eq''
