Commit 2023-05-19 11:12 8ec526bb

View on Github →

feat: port RingTheory.Localization.AtPrime (#4086)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/AtPrime.lean

added def Ideal.primeCompl

added theorem Ideal.primeCompl_le_nonZeroDivisors

added theorem IsLocalization.AtPrime.Nontrivial

added theorem IsLocalization.AtPrime.comap_maximalIdeal

added theorem IsLocalization.AtPrime.isUnit_mk'_iff

added theorem IsLocalization.AtPrime.isUnit_to_map_iff

added theorem IsLocalization.AtPrime.localRing

added theorem IsLocalization.AtPrime.mk'_mem_maximal_iff

added theorem IsLocalization.AtPrime.to_map_mem_maximal_iff

added theorem Localization.AtPrime.comap_maximalIdeal

added theorem Localization.AtPrime.map_eq_maximalIdeal

added theorem Localization.le_comap_primeCompl_iff

added theorem Localization.localRingHom_comp

added theorem Localization.localRingHom_id

added theorem Localization.localRingHom_mk'

added theorem Localization.localRingHom_to_map

added theorem Localization.localRingHom_unique