Commit 2023-05-16 18:39 41d747a5

View on Github →

feat: port Algebra.Module.LocalizedModule (#3993)

depends on: #3414

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/LocalizedModule.lean

added theorem IsLocalizedModule.eq_iff_exists

added theorem IsLocalizedModule.eq_zero_iff

added theorem IsLocalizedModule.fromLocalizedModule'_add

added theorem IsLocalizedModule.fromLocalizedModule'_mk

added theorem IsLocalizedModule.fromLocalizedModule'_smul

added theorem IsLocalizedModule.fromLocalizedModule.bij

added theorem IsLocalizedModule.fromLocalizedModule.inj

added theorem IsLocalizedModule.fromLocalizedModule.surj

added theorem IsLocalizedModule.fromLocalizedModule_mk

added theorem IsLocalizedModule.is_universal

added theorem IsLocalizedModule.iso_apply_mk

added theorem IsLocalizedModule.iso_symm_apply'

added theorem IsLocalizedModule.iso_symm_apply_aux

added theorem IsLocalizedModule.iso_symm_comp

added theorem IsLocalizedModule.lift_comp

added theorem IsLocalizedModule.lift_unique

added theorem IsLocalizedModule.mk'_add

added theorem IsLocalizedModule.mk'_add_mk'

added theorem IsLocalizedModule.mk'_cancel'

added theorem IsLocalizedModule.mk'_cancel

added theorem IsLocalizedModule.mk'_cancel_left

added theorem IsLocalizedModule.mk'_cancel_right

added theorem IsLocalizedModule.mk'_eq_iff

added theorem IsLocalizedModule.mk'_eq_mk'_iff

added theorem IsLocalizedModule.mk'_eq_zero'

added theorem IsLocalizedModule.mk'_eq_zero

added theorem IsLocalizedModule.mk'_mul_mk'

added theorem IsLocalizedModule.mk'_mul_mk'_of_map_mul

added theorem IsLocalizedModule.mk'_neg

added theorem IsLocalizedModule.mk'_one

added theorem IsLocalizedModule.mk'_smul

added theorem IsLocalizedModule.mk'_sub

added theorem IsLocalizedModule.mk'_sub_mk'

added theorem IsLocalizedModule.mk'_surjective

added theorem IsLocalizedModule.mk'_zero

added theorem IsLocalizedModule.mkOfAlgebra

added theorem IsLocalizedModule.mk_eq_mk'

added theorem IsLocalizedModule.ringHom_ext

added theorem IsLocalizedModule.smul_inj

added theorem IsLocalizedModule.smul_injective

added theorem IsLocalizedModule.surj

added theorem LocalizedModule.algebraMap_mk

added def LocalizedModule.divBy

added theorem LocalizedModule.divBy_mul_by

added theorem LocalizedModule.induction_on

added theorem LocalizedModule.induction_on₂

added theorem LocalizedModule.lift'_add

added theorem LocalizedModule.lift'_mk

added theorem LocalizedModule.lift'_smul

added def LocalizedModule.liftOn

added theorem LocalizedModule.liftOn_mk

added def LocalizedModule.liftOn₂

added theorem LocalizedModule.liftOn₂_mk

added theorem LocalizedModule.lift_comp

added theorem LocalizedModule.lift_mk

added theorem LocalizedModule.lift_unique

added def LocalizedModule.mk

added def LocalizedModule.mkLinearMap

added theorem LocalizedModule.mk_add_mk

added theorem LocalizedModule.mk_cancel

added theorem LocalizedModule.mk_cancel_common_left

added theorem LocalizedModule.mk_cancel_common_right

added theorem LocalizedModule.mk_eq

added theorem LocalizedModule.mk_mul_mk

added theorem LocalizedModule.mk_neg

added theorem LocalizedModule.mk_smul_mk

added theorem LocalizedModule.mul_by_divBy

added theorem LocalizedModule.r.isEquiv

added def LocalizedModule.r

added theorem LocalizedModule.smul'_mk

added theorem LocalizedModule.zero_mk

added def LocalizedModule