Commit 2024-10-15 07:35 427742c4

View on Github →

chore(RingTheory/Localization/Basic): split off Defs (#17735) This PR splits off a RingTheory.Localization.Defs file that is supposed to contain the definition of IsLocalization and the ring structure on Localization, and some basic results that don't need further imports. I am quite sure that we can minimize the transitive imports a bit further but this seems like a decent point to stop for now.

Estimated changes

deleted theorem IsLocalization.at_units
deleted theorem IsLocalization.eq_iff_eq
deleted theorem IsLocalization.eq_of_eq
deleted theorem IsLocalization.lift_comp
deleted theorem IsLocalization.lift_eq
deleted theorem IsLocalization.lift_id
deleted theorem IsLocalization.lift_mk'
deleted theorem IsLocalization.map_comp
deleted theorem IsLocalization.map_eq
deleted theorem IsLocalization.map_id
deleted theorem IsLocalization.map_id_mk'
deleted theorem IsLocalization.map_map
deleted theorem IsLocalization.map_mk'
deleted theorem IsLocalization.map_smul
deleted theorem IsLocalization.map_unique
deleted theorem IsLocalization.map_units
deleted theorem IsLocalization.mk'_add
deleted theorem IsLocalization.mk'_cancel
deleted theorem IsLocalization.mk'_mul
deleted theorem IsLocalization.mk'_one
deleted theorem IsLocalization.mk'_pow
deleted theorem IsLocalization.mk'_sec
deleted theorem IsLocalization.mk'_self''
deleted theorem IsLocalization.mk'_self'
deleted theorem IsLocalization.mk'_self
deleted theorem IsLocalization.mk'_spec'
deleted theorem IsLocalization.mk'_spec
deleted theorem IsLocalization.mk'_zero
deleted theorem IsLocalization.of_le
deleted theorem IsLocalization.sec_spec'
deleted theorem IsLocalization.sec_spec
deleted theorem IsLocalization.smul_mk'
deleted theorem IsLocalization.surj
deleted theorem IsLocalization.surj₂
deleted theorem Localization.add_mk
deleted theorem Localization.add_mk_self
deleted theorem Localization.mk_eq_mk'
deleted theorem Localization.mk_list_sum
deleted theorem Localization.mk_sum
deleted theorem Localization.neg_mk
deleted theorem Localization.sub_mk
added theorem IsLocalization.lift_eq
added theorem IsLocalization.lift_id
added theorem IsLocalization.map_eq
added theorem IsLocalization.map_id
added theorem IsLocalization.map_map
added theorem IsLocalization.map_mk'
added theorem IsLocalization.mk'_add
added theorem IsLocalization.mk'_mul
added theorem IsLocalization.mk'_one
added theorem IsLocalization.mk'_pow
added theorem IsLocalization.mk'_sec
added theorem IsLocalization.of_le
added theorem IsLocalization.surj
added theorem IsLocalization.surj₂
added theorem Localization.add_mk
added theorem Localization.mk_eq_mk'
added theorem Localization.mk_sum
added theorem Localization.neg_mk
added theorem Localization.sub_mk