Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-02 06:01 8026ea8a

View on Github →

feat(ring_theory/localization): localization away from an element (#4019)

Estimated changes

Modified src/group_theory/monoid_localization.lean

added theorem add_submonoid.localization_map.away_map.lift_comp

added theorem add_submonoid.localization_map.away_map.lift_eq

added def localization.away.inv_self

added theorem localization.away.mk_eq_monoid_of_mk'

added def localization.away.monoid_of

added def localization.away

added theorem submonoid.localization_map.away_map.lift_comp

added theorem submonoid.localization_map.away_map.lift_eq

added def submonoid.localization_map.away_map

modified theorem submonoid.localization_map.mk'_self'

modified theorem submonoid.localization_map.mk'_self

Modified src/ring_theory/jacobson.lean

deleted theorem ideal.disjoint_closure_singleton_iff_not_mem

added theorem ideal.disjoint_powers_iff_not_mem

Modified src/ring_theory/localization.lean

added theorem localization.away.mk_eq_mk'

added def localization.away.of

added theorem localization_map.away_map.lift_comp

added theorem localization_map.away_map.lift_eq

added def localization_map.away_map