nontrivial — Mathlib

English

If I is the top ideal, then the quotient R/I is a singleton; equivalently, R/⊤ contains exactly one element.

Русский

Если I — верхний идеал, то фактор-кольцо R/I содержит ровно один элемент; эквивалентно тому, что в R/⊤ всего один элемент.

LaTeX

$$$|R / \top| = 1$$$

Lean4

protected theorem nontrivial (hI : I ≠ ⊤) : Nontrivial (R ⧸ I) :=
  ⟨⟨0, 1, zero_ne_one_iff.2 hI⟩⟩

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