Commit 2023-03-09 14:54 0e402e90

View on Github →

feat: port/RingTheory.Localization.Basic (#2741)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/Equiv.lean

modified theorem RingEquiv.coe_ringHom_refl

added theorem RingEquiv.symm_refl

Created Mathlib/RingTheory/Localization/Basic.lean

added theorem Field.localization_map_bijective

added theorem IsField.localization_map_bijective

added theorem IsLocalization.algEquiv_mk'

added theorem IsLocalization.algEquiv_symm_mk'

added theorem IsLocalization.algHom_subsingleton

added theorem IsLocalization.algebraMap_apply_eq_map_map_submonoid

added theorem IsLocalization.algebraMap_eq_map_map_submonoid

added theorem IsLocalization.algebraMap_mk'

added theorem IsLocalization.eq_iff_eq

added theorem IsLocalization.eq_iff_exists

added theorem IsLocalization.eq_mk'_iff_mul_eq

added theorem IsLocalization.eq_of_eq

added theorem IsLocalization.eq_zero_of_fst_eq_zero

added theorem IsLocalization.isDomain_localization

added theorem IsLocalization.isDomain_of_le_nonZeroDivisors

added theorem IsLocalization.isLocalization_iff_of_algEquiv

added theorem IsLocalization.isLocalization_iff_of_base_ringEquiv

added theorem IsLocalization.isLocalization_iff_of_ringEquiv

added theorem IsLocalization.isLocalization_of_algEquiv

added theorem IsLocalization.isLocalization_of_base_ringEquiv

added theorem IsLocalization.isUnit_comp

added theorem IsLocalization.lift_algebraMap_eq_algebraMap

added theorem IsLocalization.lift_comp

added theorem IsLocalization.lift_eq

added theorem IsLocalization.lift_eq_iff

added theorem IsLocalization.lift_id

added theorem IsLocalization.lift_injective_iff

added theorem IsLocalization.lift_mk'

added theorem IsLocalization.lift_mk'_spec

added theorem IsLocalization.lift_of_comp

added theorem IsLocalization.lift_spec_mul_add

added theorem IsLocalization.lift_surjective_iff

added theorem IsLocalization.lift_unique

added theorem IsLocalization.map_comp

added theorem IsLocalization.map_comp_map

added theorem IsLocalization.map_eq

added theorem IsLocalization.map_eq_zero_iff

added theorem IsLocalization.map_id

added theorem IsLocalization.map_id_mk'

added theorem IsLocalization.map_injective_of_injective

added theorem IsLocalization.map_left_cancel

added theorem IsLocalization.map_map

added theorem IsLocalization.map_mk'

added theorem IsLocalization.map_nonZeroDivisors_le

added theorem IsLocalization.map_right_cancel

added theorem IsLocalization.map_smul

added theorem IsLocalization.map_unique

added theorem IsLocalization.map_units

added theorem IsLocalization.map_units_map_submonoid

added theorem IsLocalization.mk'_add

added theorem IsLocalization.mk'_add_eq_iff_add_mul_eq_mul

added theorem IsLocalization.mk'_eq_iff_eq'

added theorem IsLocalization.mk'_eq_iff_eq

added theorem IsLocalization.mk'_eq_iff_eq_mul

added theorem IsLocalization.mk'_eq_iff_mk'_eq

added theorem IsLocalization.mk'_eq_mul_mk'_one

added theorem IsLocalization.mk'_eq_of_eq'

added theorem IsLocalization.mk'_eq_of_eq

added theorem IsLocalization.mk'_eq_zero_iff

added theorem IsLocalization.mk'_mem_iff

added theorem IsLocalization.mk'_mul

added theorem IsLocalization.mk'_mul_cancel_left

added theorem IsLocalization.mk'_mul_cancel_right

added theorem IsLocalization.mk'_mul_mk'_eq_one'

added theorem IsLocalization.mk'_mul_mk'_eq_one

added theorem IsLocalization.mk'_one

added theorem IsLocalization.mk'_sec

added theorem IsLocalization.mk'_self''

added theorem IsLocalization.mk'_self'

added theorem IsLocalization.mk'_self

added theorem IsLocalization.mk'_spec'

added theorem IsLocalization.mk'_spec'_mk

added theorem IsLocalization.mk'_spec

added theorem IsLocalization.mk'_spec_mk

added theorem IsLocalization.mk'_surjective

added theorem IsLocalization.mk'_zero

added theorem IsLocalization.monoidHom_ext

added theorem IsLocalization.mul_add_inv_left

added theorem IsLocalization.mul_mk'_eq_mk'_of_mul

added theorem IsLocalization.ne_zero_of_mk'_ne_zero

added theorem IsLocalization.noZeroDivisors_of_le_nonZeroDivisors

added theorem IsLocalization.nonZeroDivisors_le_comap

added theorem IsLocalization.of_le

added theorem IsLocalization.ringEquivOfRingEquiv_eq

added theorem IsLocalization.ringEquivOfRingEquiv_eq_map

added theorem IsLocalization.ringEquivOfRingEquiv_mk'

added theorem IsLocalization.ringHom_ext

added theorem IsLocalization.sec_fst_ne_zero

added theorem IsLocalization.sec_snd_ne_zero

added theorem IsLocalization.sec_spec'

added theorem IsLocalization.sec_spec

added theorem IsLocalization.surj

added theorem IsLocalization.toLocalizationMap_sec

added theorem IsLocalization.toLocalizationMap_toMap

added theorem IsLocalization.toLocalizationMap_toMap_apply

added def IsLocalization.toLocalizationWithZeroMap

added theorem IsLocalization.to_map_eq_zero_iff

added def IsLocalization.uniqueOfZeroMem

added theorem Localization.add_mk

added theorem Localization.add_mk_self

added theorem Localization.algEquiv_mk

added theorem Localization.algEquiv_symm_mk

added def Localization.mkAddMonoidHom

added theorem Localization.mk_algebraMap

added theorem Localization.mk_eq_mk'

added theorem Localization.mk_eq_mk'_apply

added theorem Localization.mk_int_cast

added theorem Localization.mk_list_sum

added theorem Localization.mk_multiset_sum

added theorem Localization.mk_nat_cast

added theorem Localization.mk_one_eq_algebraMap

added theorem Localization.mk_sum

added theorem Localization.monoidOf_eq_algebraMap

added theorem Localization.neg_mk

added theorem Localization.sub_mk

added theorem Localization.toLocalizationMap_eq_monoidOf

added theorem localizationAlgebra_injective