minimalPrimes_eq_minimals — Mathlib

English

In a commutative semiring R, the set of minimal prime ideals equals the set of prime ideals that are minimal with respect to inclusion among prime ideals.

Русский

В коммутативном полукольце R множество минимальных простых идеалов равно множеству простых идеалов, минимальных по включению среди простых идеалов.

LaTeX

$$$\minPrimes(R) = \{ p \subseteq R \mid p \text{ is a minimal prime ideal} \}$$$

Lean4

theorem minimalPrimes_eq_minimals : minimalPrimes R = {x | Minimal Ideal.IsPrime x} :=
  congr_arg Minimal (by simp)

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