Commit 2024-04-23 03:32 a1bf7622

View on Github →

chore: split out Ideal.IsPrimary (#12296) This splits out a small but self-contained part of RingTheory.Ideal.Operations.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Ideal/AssociatedPrime.lean

Created Mathlib/RingTheory/Ideal/IsPrimary.lean

added def Ideal.IsPrimary

added theorem Ideal.IsPrime.isPrimary

added theorem Ideal.isPrimary_inf

added theorem Ideal.isPrime_radical

added theorem Ideal.mem_radical_of_pow_mem

Modified Mathlib/RingTheory/Ideal/MinimalPrime.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

deleted def Ideal.IsPrimary

deleted theorem Ideal.IsPrime.isPrimary

deleted theorem Ideal.isPrimary_inf

deleted theorem Ideal.isPrime_radical

deleted theorem Ideal.mem_radical_of_pow_mem

Modified Mathlib/RingTheory/JacobsonIdeal.lean