mk_eq_mk_iff_sub_mem

Mathlib.RingTheory.Ideal.Quotient.Defs

URI: https://scilib.ai/kg/mathlib#Ideal.Quotient.mk_eq_mk_iff_sub_mem

English

mk I x = mk I y iff x - y ∈ I.

Русский

mk I x = mk I y тогда и только тогда, когда x - y ∈ I.

LaTeX

$$$\\pi_I(x) = \\pi_I(y) \\iff x-y \\in I$$$

Lean4

theorem mk_eq_mk_iff_sub_mem (x y : R) : mk I x = mk I y ↔ x - y ∈ I := by rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]

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

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

Разделы

Аффилиация

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