instNonemptyOfNontrivial — Mathlib

English

If R is a nontrivial commutative semiring, then there exists a maximal ideal of R.

Русский

Если R — не тривиальное коммутативное полукольцо, то существует максимальный идеал в R.

LaTeX

$$$\exists \mathfrak m \;\bigl( \mathfrak m \in \mathrm{Ideal}(R) \wedge \mathfrak m \text{ maximal} \bigr)$$$

Lean4

instance [Nontrivial R] : Nonempty <| MaximalSpectrum R :=
  let ⟨I, hI⟩ := Ideal.exists_maximal R
  ⟨⟨I, hI⟩⟩

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