Commit 2024-01-23 00:09 99315bf7

View on Github →

feat(Algebra/AddConstMap): new file (#9725)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/AddConstMap/Basic.lean

added def AddConstMap.addLeftHom

added theorem AddConstMap.coe_mk

added theorem AddConstMap.coe_mul

added theorem AddConstMap.coe_one

added theorem AddConstMap.coe_pow

added theorem AddConstMap.coe_vadd

added def AddConstMap.comp

added theorem AddConstMap.comp_id

added def AddConstMap.conjNeg

added theorem AddConstMap.conjNeg_symm

added theorem AddConstMap.id_comp

added def AddConstMap.mkFract

added theorem AddConstMap.mk_coe

added theorem AddConstMap.mul_def

added theorem AddConstMap.one_def

added theorem AddConstMap.pow_apply

added def AddConstMap.replaceConsts

added def AddConstMap.smul

added structure AddConstMap

added theorem AddConstMapClass.antitone_iff_Icc

added theorem AddConstMapClass.map_add_int'

added theorem AddConstMapClass.map_add_int

added theorem AddConstMapClass.map_add_nat'

added theorem AddConstMapClass.map_add_nat

added theorem AddConstMapClass.map_add_nsmul

added theorem AddConstMapClass.map_add_ofNat'

added theorem AddConstMapClass.map_add_ofNat

added theorem AddConstMapClass.map_add_one

added theorem AddConstMapClass.map_add_zsmul

added theorem AddConstMapClass.map_const

added theorem AddConstMapClass.map_const_add

added theorem AddConstMapClass.map_fract

added theorem AddConstMapClass.map_int_add'

added theorem AddConstMapClass.map_int_add

added theorem AddConstMapClass.map_nat'

added theorem AddConstMapClass.map_nat

added theorem AddConstMapClass.map_nat_add'

added theorem AddConstMapClass.map_nat_add

added theorem AddConstMapClass.map_nsmul_add

added theorem AddConstMapClass.map_nsmul_const

added theorem AddConstMapClass.map_ofNat'

added theorem AddConstMapClass.map_ofNat

added theorem AddConstMapClass.map_ofNat_add'

added theorem AddConstMapClass.map_ofNat_add

added theorem AddConstMapClass.map_one

added theorem AddConstMapClass.map_one_add

added theorem AddConstMapClass.map_sub_const

added theorem AddConstMapClass.map_sub_int'

added theorem AddConstMapClass.map_sub_int

added theorem AddConstMapClass.map_sub_nat'

added theorem AddConstMapClass.map_sub_nsmul

added theorem AddConstMapClass.map_sub_ofNat'

added theorem AddConstMapClass.map_sub_one

added theorem AddConstMapClass.map_sub_zsmul

added theorem AddConstMapClass.map_zsmul_add

added theorem AddConstMapClass.map_zsmul_const

added theorem AddConstMapClass.monotone_iff_Icc

added theorem AddConstMapClass.strictAnti_iff_Icc

added theorem AddConstMapClass.strictMono_iff_Icc