minimalPrimes — Mathlib

English

For a ring R, the set of minimal prime ideals over a given ideal I is defined as the set of primes p that are minimal among primes containing I.

Русский

Для кольца R множество минимальных простых идеалов над I — это простые идеалы p, минимальные над I.

LaTeX

$$$\\text{minimalPrimes}(R,I) = \\{ p\\in \\text{I}(R) : p \\text{ prime and } I \\subseteq p, \\text{ и минимальны среди таких } p\\}$$$

Lean4

/-- `I.minimalPrimes` is the set of ideals that are minimal primes over `I`. -/
protected def minimalPrimes : Set (Ideal R) :=
  {p | Minimal (fun q ↦ q.IsPrime ∧ I ≤ q) p}

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