eq

Mathlib.RingTheory.Ideal.Quotient.Defs

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

English

Equality of two quotient representatives corresponds to their difference lying in I.

Русский

Равенство представителей в фактор-кольце эквивалентно тому, что их разность принадлежит I.

LaTeX

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

Lean4

protected theorem eq : mk I x = mk I y ↔ x - y ∈ I :=
  Submodule.Quotient.eq I

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

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

Разделы

Аффилиация

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