Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-04 15:38 add0c9a8

View on Github →

feat(ring/localization): add construction of localization as a quotient type (#2922)

Estimated changes

Modified src/group_theory/congruence.lean

Modified src/group_theory/monoid_localization.lean

added theorem localization.ind

added theorem localization.induction_on

added theorem localization.induction_on₂

added theorem localization.induction_on₃

added def localization.mk

added theorem localization.mk_eq_monoid_of_mk'

added theorem localization.mk_eq_monoid_of_mk'_apply

added theorem localization.mk_one_eq_monoid_of_mk

added def localization.monoid_of

added theorem localization.mul_equiv_of_quotient_apply

added theorem localization.mul_equiv_of_quotient_mk'

added theorem localization.mul_equiv_of_quotient_mk

added theorem localization.mul_equiv_of_quotient_monoid_of

added theorem localization.mul_equiv_of_quotient_symm_mk'

added theorem localization.mul_equiv_of_quotient_symm_mk

added theorem localization.mul_equiv_of_quotient_symm_monoid_of

added theorem localization.one_rel

added def localization.r'

added def localization.r

added theorem localization.r_eq_r'

added theorem localization.r_iff_exists

added theorem localization.r_of_eq

added def localization

deleted def submonoid.localization.r'

deleted def submonoid.localization.r

deleted theorem submonoid.localization.r_eq_r'

deleted theorem submonoid.localization.r_iff_exists

deleted def submonoid.localization

Modified src/ring_theory/fractional_ideal.lean

Modified src/ring_theory/localization.lean

modified def fraction_map

deleted def localization.codomain

deleted theorem localization.epic_of_localization_map

deleted theorem localization.eq_iff_eq

deleted theorem localization.eq_iff_exists

deleted theorem localization.eq_mk'_iff_mul_eq

deleted theorem localization.eq_of_eq

deleted theorem localization.eq_zero_of_fst_eq_zero

deleted theorem localization.exists_integer_multiple'

deleted theorem localization.exists_integer_multiple

deleted theorem localization.ext

deleted theorem localization.ext_iff

deleted def localization.is_integer

deleted theorem localization.is_integer_add

deleted theorem localization.is_integer_mul

deleted theorem localization.is_integer_smul

deleted theorem localization.is_unit_comp

deleted theorem localization.lift_comp

deleted theorem localization.lift_eq

deleted theorem localization.lift_eq_iff

deleted theorem localization.lift_id

deleted theorem localization.lift_injective_iff

deleted theorem localization.lift_left_inverse

deleted theorem localization.lift_mk'

deleted theorem localization.lift_mk'_spec

deleted theorem localization.lift_of_comp

deleted theorem localization.lift_surjective_iff

deleted theorem localization.lift_unique

deleted def localization.lin_coe

deleted theorem localization.lin_coe_apply

deleted theorem localization.map_comp

deleted theorem localization.map_comp_map

deleted theorem localization.map_eq

deleted theorem localization.map_id

deleted theorem localization.map_left_cancel

deleted theorem localization.map_map

deleted theorem localization.map_mk'

deleted theorem localization.map_right_cancel

deleted theorem localization.map_units

deleted theorem localization.mem_coe

deleted theorem localization.mk'_add

deleted theorem localization.mk'_eq_iff_eq

deleted theorem localization.mk'_eq_iff_eq_mul

deleted theorem localization.mk'_eq_iff_mk'_eq

deleted theorem localization.mk'_eq_mul_mk'_one

deleted theorem localization.mk'_eq_of_eq

deleted theorem localization.mk'_mul

deleted theorem localization.mk'_mul_cancel_left

deleted theorem localization.mk'_mul_cancel_right

deleted theorem localization.mk'_one

deleted theorem localization.mk'_sec

deleted theorem localization.mk'_self''

deleted theorem localization.mk'_self'

deleted theorem localization.mk'_self

deleted theorem localization.mk'_spec'

deleted theorem localization.mk'_spec

added theorem localization.mk_eq_mk'

added theorem localization.mk_eq_mk'_apply

added theorem localization.mk_one_eq_of

added theorem localization.monoid_of_eq_of

deleted theorem localization.mul_mk'_eq_mk'_of_mul

added def localization.of

deleted theorem localization.of_id

added theorem localization.ring_equiv_of_quotient_apply

added theorem localization.ring_equiv_of_quotient_mk'

added theorem localization.ring_equiv_of_quotient_mk

added theorem localization.ring_equiv_of_quotient_of

added theorem localization.ring_equiv_of_quotient_symm_mk'

added theorem localization.ring_equiv_of_quotient_symm_mk

added theorem localization.ring_equiv_of_quotient_symm_of

deleted theorem localization.ring_equiv_of_ring_equiv_eq

deleted theorem localization.ring_equiv_of_ring_equiv_eq_map

deleted theorem localization.ring_equiv_of_ring_equiv_eq_map_apply

deleted theorem localization.ring_equiv_of_ring_equiv_mk'

deleted theorem localization.sec_spec'

deleted theorem localization.sec_spec

deleted theorem localization.surj

deleted def localization.to_map

deleted theorem localization.to_map_injective

deleted structure localization

added def localization_map.codomain

added theorem localization_map.epic_of_localization_map

added theorem localization_map.eq_iff_eq

added theorem localization_map.eq_iff_exists

added theorem localization_map.eq_mk'_iff_mul_eq

added theorem localization_map.eq_of_eq

added theorem localization_map.eq_zero_of_fst_eq_zero

added theorem localization_map.exists_integer_multiple'

added theorem localization_map.exists_integer_multiple

added theorem localization_map.ext

added theorem localization_map.ext_iff

added def localization_map.is_integer

added theorem localization_map.is_integer_add

added theorem localization_map.is_integer_mul

added theorem localization_map.is_integer_smul

added theorem localization_map.is_unit_comp

added theorem localization_map.lift_comp

added theorem localization_map.lift_eq

added theorem localization_map.lift_eq_iff

added theorem localization_map.lift_id

added theorem localization_map.lift_injective_iff

added theorem localization_map.lift_left_inverse

added theorem localization_map.lift_mk'

added theorem localization_map.lift_mk'_spec

added theorem localization_map.lift_of_comp

added theorem localization_map.lift_surjective_iff

added theorem localization_map.lift_unique

added def localization_map.lin_coe

added theorem localization_map.lin_coe_apply

added theorem localization_map.map_comp

added theorem localization_map.map_comp_map

added theorem localization_map.map_eq

added theorem localization_map.map_id

added theorem localization_map.map_left_cancel

added theorem localization_map.map_map

added theorem localization_map.map_mk'

added theorem localization_map.map_right_cancel

added theorem localization_map.map_units

added theorem localization_map.mem_coe

added theorem localization_map.mk'_add

added theorem localization_map.mk'_eq_iff_eq

added theorem localization_map.mk'_eq_iff_eq_mul

added theorem localization_map.mk'_eq_iff_mk'_eq

added theorem localization_map.mk'_eq_mul_mk'_one

added theorem localization_map.mk'_eq_of_eq

added theorem localization_map.mk'_mul

added theorem localization_map.mk'_mul_cancel_left

added theorem localization_map.mk'_mul_cancel_right

added theorem localization_map.mk'_one

added theorem localization_map.mk'_sec

added theorem localization_map.mk'_self''

added theorem localization_map.mk'_self'

added theorem localization_map.mk'_self

added theorem localization_map.mk'_spec'

added theorem localization_map.mk'_spec

added theorem localization_map.mul_mk'_eq_mk'_of_mul

added theorem localization_map.of_id

added theorem localization_map.ring_equiv_of_ring_equiv_eq

added theorem localization_map.ring_equiv_of_ring_equiv_eq_map

added theorem localization_map.ring_equiv_of_ring_equiv_eq_map_apply

added theorem localization_map.ring_equiv_of_ring_equiv_mk'

added theorem localization_map.sec_spec'

added theorem localization_map.sec_spec

added theorem localization_map.surj

added def localization_map.to_map

added theorem localization_map.to_map_injective

added structure localization_map

deleted def ring_hom.to_localization

added def ring_hom.to_localization_map

added def submonoid.localization_map.to_ring_localization