subsingleton_iff — Mathlib

English

The quotient R/I is a singleton if and only if I equals ⊤; equivalently, the quotient is subsingleton exactly when the ideal is the whole ring.

Русский

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

LaTeX

$$$\mathrm{Subsingleton}(R/I) \iff I = \top$$$

Lean4

theorem subsingleton_iff : Subsingleton (R ⧸ I) ↔ I = ⊤ :=
  by
  rw [Submodule.Quotient.subsingleton_iff, eq_top_iff, SetLike.le_def]
  simp_rw [Submodule.mem_top, true_implies]

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