Commit 2023-05-21 15:37 67e16b06

View on Github →

feat: port RingTheory.Ideal.MinimalPrime (#4146) Please feel free to push changes to this branch.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/MinimalPrime.lean

added theorem Ideal.comap_minimalPrimes_eq_of_surjective

added theorem Ideal.exists_comap_eq_of_mem_minimalPrimes

added theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective

added theorem Ideal.exists_minimalPrimes_comap_eq

added theorem Ideal.exists_minimalPrimes_le

added theorem Ideal.mimimal_primes_comap_of_surjective

added theorem Ideal.minimalPrimes_eq_comap

added theorem Ideal.minimalPrimes_eq_subsingleton

added theorem Ideal.minimalPrimes_eq_subsingleton_self

added theorem Ideal.radical_minimalPrimes

added theorem Ideal.sInf_minimalPrimes

added def minimalPrimes

Modified Mathlib/RingTheory/Localization/Basic.lean