Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-06 12:39 d2428fae

View on Github →

feat(ring_theory/localization): Localization is the localization of localization. (#11145)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.exists_image_iff

Modified src/ring_theory/localization.lean

added theorem is_localization.is_localization_of_is_exists_mul_mem

added theorem is_localization.is_localization_of_submonoid_le

added def is_localization.localization_algebra_of_submonoid_le

added theorem is_localization.localization_is_scalar_tower_of_submonoid_le