Commit 2023-05-22 03:13 eec62fe5

View on Github →

feat: port RingTheory.Localization.LocalizationLocalization (#4137)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Localization/LocalizationLocalization.lean

added theorem IsFractionRing.isFractionRing_of_isDomain_of_isLocalization

added theorem IsFractionRing.isFractionRing_of_isLocalization

added theorem IsLocalization.isLocalization_isLocalization_atPrime_isLocalization

added theorem IsLocalization.isLocalization_of_is_exists_mul_mem

added theorem IsLocalization.isLocalization_of_submonoid_le

added def IsLocalization.localizationLocalizationSubmodule

added theorem IsLocalization.localization_isScalarTower_of_submonoid_le

added theorem IsLocalization.localization_localization_eq_iff_exists

added theorem IsLocalization.localization_localization_isLocalization

added theorem IsLocalization.localization_localization_isLocalization_of_has_all_units

added theorem IsLocalization.localization_localization_map_units

added theorem IsLocalization.localization_localization_surj

added theorem IsLocalization.mem_localizationLocalizationSubmodule