Prime ideals #
This file contains the definition of Ideal.IsPrime
for prime ideals.
TODO #
Support right ideals, and two-sided ideals over non-commutative rings.
An ideal P
of a ring R
is prime if P ≠ R
and xy ∈ P → x ∈ P ∨ y ∈ P
The prime ideal is not the entire ring.
If a product lies in the prime ideal, then at least one element lies in the prime ideal.
Instances
The complement of a prime ideal P ⊆ R
is a submonoid of R
.
Equations
- P.primeCompl = { carrier := (↑P)ᶜ, mul_mem' := ⋯, one_mem' := ⋯ }