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

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

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

theorem Ideal.mem_radical_of_pow_mem {R : Type u_1} [CommSemiring R] {I : Ideal R} {x : R} {m : ℕ} (hx : x ^ m ∈ Ideal.radical I) : x ∈ Ideal.radical I

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

theorem Ideal.isPrimary_inf {R : Type u_1} [CommSemiring R] {I : Ideal R} {J : Ideal R} (hi : Ideal.IsPrimary I) (hj : Ideal.IsPrimary J) (hij : Ideal.radical I = Ideal.radical J) : Ideal.IsPrimary (I ⊓ J)