zero_ne_one_iff — Mathlib

English

Let R be a ring and I an ideal. The quotient ring R/I has 0 and 1 distinct if and only if I is not the entire ring; equivalently, the quotient is the zero ring precisely when I = ⊤.

Русский

Пусть R—кольцо и I—идеал. Фактор—кольцо R/I имеет различные 0 и 1 тогда и только тогда, когда I не равен всему кольцу; эквивалентно, фактор-кольцо тождественно нулевое тогда и только тогда, когда I = ⊤.

LaTeX

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

Lean4

theorem zero_ne_one_iff : (0 : R ⧸ I) ≠ 1 ↔ I ≠ ⊤ :=
  not_congr zero_eq_one_iff

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