Primary ideals

A proper ideal I is primary iff xy ∈ I implies x ∈ I or y ∈ radical I.

Main definitions

• Ideal.IsPrimary

def Ideal.IsPrimary {R : Type u_1} [CommSemiring R] (I : Ideal R) : Prop

A proper ideal I is primary iff xy ∈ I implies x ∈ I or y ∈ radical I.

Equations

• I.IsPrimary = (I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical)

theorem Ideal.IsPrime.isPrimary {R : Type u_1} [CommSemiring R] {I : Ideal R} (hi : I.IsPrime) : I.IsPrimary

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