coe_mk — Mathlib

English

There is an order-preserving correspondence between two-sided ideals of a ring and congruence relations on the ring (ring-congruences).

Русский

Существует взаимооднозначное соответствие между двусторонними идеалами кольца и отношениями конгруэнтности на кольце (кольцевые конгруэнции).

LaTeX

$$TwoSidedIdeal R ≃o RingCon R$$

Lean4

@[simp, norm_cast]
theorem coe_mk {c : RingCon R} : (mk c : Set R) = {x | c x 0} :=
  rfl

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