coe_inj — Mathlib

English

Two congruences are equal iff their underlying binary relations are equal.

Русский

Две конгруэнции равны тогда и только тогда, когда их бинарные отношения равны.

LaTeX

$$$(\\uparrow c = \\uparrow d) \\iff c = d$$$

Lean4

/-- Two congruence relations are equal iff their underlying binary relations are equal. -/
@[to_additive /-- Two additive congruence relations are equal iff their underlying binary relations
    are equal. -/
    ]
theorem coe_inj {c d : Con M} : ⇑c = ⇑d ↔ c = d :=
  DFunLike.coe_injective.eq_iff

Похожие утверждения