ringCon_le_iff

Mathlib.RingTheory.TwoSidedIdeal.Basic

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.ringCon_le_iff

English

Equivalent reformulation of the order isomorphism, asserting equivalence of ≤ for ring-congruences and for ideals.

Русский

Повторное утверждение: неравенство конгруэнций соответствует неравенству идеалов.

LaTeX

$$I ≤ J ↔ I.ringCon ≤ J.ringCon$$

Lean4

theorem ringCon_le_iff {I J : TwoSidedIdeal R} : I ≤ J ↔ I.ringCon ≤ J.ringCon :=
  orderIsoRingCon.map_rel_iff.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru