isEmpty_iff_subsingleton — Mathlib

English

For commutative semirings R, PrimeSpectrum R is empty if and only if R is subsingleton.

Русский

Для коммутативного полукольца R спектр простых пуст, если и только если R—подпоследовательность (subsingleton).

LaTeX

$$$\\operatorname{IsEmpty}(\\\\operatorname{PrimeSpectrum}(R)) \\\\iff \\\\operatorname{Subsingleton}(R)$$$

Lean4

theorem isEmpty_iff_subsingleton : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
  rw [← not_iff_not, not_isEmpty_iff, not_subsingleton_iff_nontrivial, nonempty_iff_nontrivial]

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