Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-04 19:11 023d4f7d

View on Github →

feat(ring_theory/localization): order embedding of ideals, local ring instance (#3287)

Estimated changes

Modified src/ring_theory/fractional_ideal.lean

Modified src/ring_theory/localization.lean

added def ideal.prime_compl

added def localization.at_prime

added def localization_map.at_prime

modified def localization_map.codomain

added def localization_map.le_order_embedding

added theorem localization_map.map_comap

added theorem localization_map.mk'_mul_mk'_eq_one'

added theorem localization_map.mk'_mul_mk'_eq_one

modified theorem localization_map.mk'_self

added theorem localization_map.mk'_surjective