Primary ideals #
A proper ideal I
is primary iff xy ∈ I
implies x ∈ I
or y ∈ radical I
.
Main definitions #
theorem
Ideal.IsPrime.isPrimary
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
(hi : I.IsPrime)
:
I.IsPrimary
theorem
Ideal.mem_radical_of_pow_mem
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
{x : R}
{m : ℕ}
(hx : x ^ m ∈ I.radical)
:
x ∈ I.radical
theorem
Ideal.isPrime_radical
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
(hi : I.IsPrimary)
:
I.radical.IsPrime
theorem
Ideal.isPrimary_inf
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
{J : Ideal R}
(hi : I.IsPrimary)
(hj : J.IsPrimary)
(hij : I.radical = J.radical)
:
(I ⊓ J).IsPrimary