nonempty_iff_nontrivial — Mathlib

English

For a commutative semiring R, the prime spectrum is nonempty if and only if R is nontrivial.

Русский

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

LaTeX

$$$\\\\operatorname{Nonempty}(\\\\operatorname{PrimeSpectrum}(R)) \\\\iff \\\\operatorname{Nontrivial}(R)$$$

Lean4

theorem nonempty_iff_nontrivial : Nonempty (PrimeSpectrum R) ↔ Nontrivial R :=
  by
  refine ⟨fun ⟨p⟩ ↦ ⟨0, 1, fun h ↦ p.2.ne_top ?_⟩, fun h ↦ ?_⟩
  · simp [Ideal.eq_top_iff_one p.asIdeal, ← h]
  · obtain ⟨I, hI⟩ := Ideal.exists_maximal R
    exact ⟨⟨I, hI.isPrime⟩⟩

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