Commit 2023-06-15 02:56 00b77c0a

View on Github →

feat: port RingTheory.LocalProperties (#5010)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/LocalProperties.lean

added theorem Ideal.eq_of_localization_maximal

added theorem Ideal.le_of_localization_maximal

added theorem IsLocalization.exists_smul_mem_of_mem_adjoin

added theorem IsLocalization.lift_mem_adjoin_finsetIntegerMultiple

added theorem IsLocalization.smul_mem_finsetIntegerMultiple_span

added def LocalizationPreserves

added def OfLocalizationMaximal

added def RingHom.HoldsForLocalizationAway

added theorem RingHom.LocalizationPreserves.away

added def RingHom.LocalizationPreserves

added def RingHom.OfLocalizationFiniteSpan

added def RingHom.OfLocalizationFiniteSpanTarget

added def RingHom.OfLocalizationPrime

added def RingHom.OfLocalizationSpan

added def RingHom.OfLocalizationSpanTarget

added theorem RingHom.PropertyIsLocal.ofLocalizationSpan

added theorem RingHom.PropertyIsLocal.respectsIso

added structure RingHom.PropertyIsLocal

added theorem RingHom.ofLocalizationSpanTarget_iff_finite

added theorem RingHom.ofLocalizationSpan_iff_finite

added theorem eq_zero_of_localization

added theorem finiteType_ofLocalizationSpan

added theorem finite_ofLocalizationSpan

added theorem ideal_eq_bot_of_localization'

added theorem ideal_eq_bot_of_localization

added theorem isReduced_ofLocalizationMaximal

added theorem localizationPreserves_surjective

added theorem localization_away_map_finite

added theorem localization_away_map_finiteType

added theorem localization_finite

added theorem localization_finiteType

added theorem localization_isReduced

added theorem multiple_mem_adjoin_of_mem_localization_adjoin

added theorem multiple_mem_span_of_mem_localization_span

added theorem surjective_ofLocalizationSpan