zero_eq_one_iff

Mathlib.RingTheory.Ideal.Quotient.Basic

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

English

In the quotient ring R/I, 0 equals 1 if and only if I is the whole ring.

Русский

В факторкольце R/I ноль равен единице тогда и только тогда, когда I = ⊤.

LaTeX

$$$(0 : R / I) = 1 \\iff I = \\top$$$

Lean4

theorem zero_eq_one_iff : (0 : R ⧸ I) = 1 ↔ I = ⊤ :=
  eq_comm.trans <| (Submodule.Quotient.mk_eq_zero _).trans (eq_top_iff_one _).symm

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

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

Разделы

Аффилиация

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