Theorems · Definition · commutative algebra

Ideal.primeCompl

{α : Type u} → [inst : Semiring α] → (P : Ideal α) → [hp : P.IsPrime] → Submonoid α

The complement of a prime ideal P ⊆ R is a submonoid of R.

Defined in

Mathlib.RingTheory.Ideal.Prime

Cited by

462 results in Mathlib

Foundations

Depth 30 from the axioms, rests on 273 definitions · uses propext, Quot.sound

Assumes

SemiringIdeal.IsPrime