ringCon_injective

Mathlib.RingTheory.TwoSidedIdeal.Basic

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

English

The order on two-sided ideals corresponds to the order on ring congruences via the isomorphism.

Русский

Порядок на двусторонних идеалах соответствует порядку конгруэнций через изоморфизм.

LaTeX

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

Lean4

theorem ringCon_injective : Function.Injective (TwoSidedIdeal.ringCon (R := R)) := by rintro ⟨x⟩ ⟨y⟩ rfl; rfl

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

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

Разделы

Аффилиация

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