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
@[deprecated Ideal.IsPrime.mul_notMem (since := "2025-05-23")]
theorem
Ideal.IsPrime.mul_not_mem
{α : Type u}
[Semiring α]
{I : Ideal α}
(hI : I.IsPrime)
{x y : α}
:
x ∉ I → y ∉ I → x * y ∉ I
Alias of Ideal.IsPrime.mul_notMem
.