Commit 2024-01-18 10:31 ff40d692

View on Github →

feat: Lemma on Monoid Localization and Consequences on Minimal Primes (#9640)

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/GroupTheory/MonoidLocalization.lean

added theorem Submonoid.LocalizationMap.map_injective_of_injective

added theorem Submonoid.LocalizationMap.mk'_eq_of_same

added theorem Submonoid.LocalizationMap.surj₂

Modified Mathlib/RingTheory/Ideal/MinimalPrime.lean

modified def minimalPrimes

modified theorem minimalPrimes_eq_minimals

Modified Mathlib/RingTheory/Localization/Basic.lean

modified theorem IsLocalization.map_injective_of_injective

added theorem IsLocalization.surj₂