Commit 2022-12-02 23:34 487ae746

View on Github →

feat: port Algebra.Hom.Group (#659) mathlib3 SHA: 8c53048add6ffacdda0b36c4917bfe37e209b0ba

depends on #563
depends on https://github.com/leanprover-community/mathlib/pull/17733
depends on https://github.com/leanprover/lean4/pull/1901
depends on https://github.com/leanprover/lean4/pull/1907

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Defs.lean

added theorem negSucc_zsmul

Created Mathlib/Algebra/Hom/Group.lean

added structure AddHom

added theorem AddMonoid.coe_mul

added theorem AddMonoid.coe_one

added structure AddMonoidHom

added theorem Monoid.coe_mul

added theorem Monoid.coe_one

added theorem MonoidHom.cancel_left

added theorem MonoidHom.cancel_right

added theorem MonoidHom.coe_coe

added theorem MonoidHom.coe_comp

added theorem MonoidHom.coe_inj

added theorem MonoidHom.coe_mk

added theorem MonoidHom.coe_of_map_div

added theorem MonoidHom.coe_of_map_mul_inv

added def MonoidHom.comp

added theorem MonoidHom.comp_apply

added theorem MonoidHom.comp_assoc

added theorem MonoidHom.comp_id

added theorem MonoidHom.comp_inv

added theorem MonoidHom.comp_mul

added theorem MonoidHom.comp_one

added theorem MonoidHom.congr_arg

added theorem MonoidHom.congr_fun

added theorem MonoidHom.div_apply

added theorem MonoidHom.ext

added theorem MonoidHom.ext_iff

added def MonoidHom.id

added theorem MonoidHom.id_comp

added theorem MonoidHom.inv_apply

added theorem MonoidHom.inv_comp

added theorem MonoidHom.map_exists_left_inv

added theorem MonoidHom.map_exists_right_inv

added def MonoidHom.mk'

added theorem MonoidHom.mk_coe

added theorem MonoidHom.mul_apply

added theorem MonoidHom.mul_comp

added def MonoidHom.ofMapDiv

added def MonoidHom.ofMapMulInv

added theorem MonoidHom.one_apply

added theorem MonoidHom.one_comp

added theorem MonoidHom.toMulHom_coe

added theorem MonoidHom.toMulHom_injective

added theorem MonoidHom.toOneHom_coe

added theorem MonoidHom.toOneHom_injective

added structure MonoidHom

added theorem MonoidWithZeroHom.cancel_left

added theorem MonoidWithZeroHom.cancel_right

added theorem MonoidWithZeroHom.coe_coe

added theorem MonoidWithZeroHom.coe_comp

added theorem MonoidWithZeroHom.coe_inj

added theorem MonoidWithZeroHom.coe_mk

added def MonoidWithZeroHom.comp

added theorem MonoidWithZeroHom.comp_apply

added theorem MonoidWithZeroHom.comp_assoc

added theorem MonoidWithZeroHom.comp_id

added theorem MonoidWithZeroHom.congr_arg

added theorem MonoidWithZeroHom.congr_fun

added theorem MonoidWithZeroHom.ext

added theorem MonoidWithZeroHom.ext_iff

added def MonoidWithZeroHom.id

added theorem MonoidWithZeroHom.id_comp

added theorem MonoidWithZeroHom.mk_coe

added theorem MonoidWithZeroHom.toMonoidHom_coe

added theorem MonoidWithZeroHom.toMonoidHom_injective

added theorem MonoidWithZeroHom.toZeroHom_coe

added theorem MonoidWithZeroHom.toZeroHom_injective

added structure MonoidWithZeroHom

added theorem MulHom.cancel_left

added theorem MulHom.cancel_right

added theorem MulHom.coe_coe

added theorem MulHom.coe_comp

added theorem MulHom.coe_inj

added theorem MulHom.coe_mk

added def MulHom.comp

added theorem MulHom.comp_apply

added theorem MulHom.comp_assoc

added theorem MulHom.comp_id

added theorem MulHom.comp_mul

added theorem MulHom.congr_arg

added theorem MulHom.congr_fun

added theorem MulHom.ext

added theorem MulHom.ext_iff

added def MulHom.id

added theorem MulHom.id_comp

added theorem MulHom.mk_coe

added theorem MulHom.mul_apply

added theorem MulHom.mul_comp

added structure MulHom

added theorem NeZero.of_injective

added theorem NeZero.of_map

added theorem OneHom.cancel_left

added theorem OneHom.cancel_right

added theorem OneHom.coe_coe

added theorem OneHom.coe_comp

added theorem OneHom.coe_inj

added theorem OneHom.coe_mk

added def OneHom.comp

added theorem OneHom.comp_apply

added theorem OneHom.comp_assoc

added theorem OneHom.comp_id

added theorem OneHom.comp_one

added theorem OneHom.congr_arg

added theorem OneHom.congr_fun

added theorem OneHom.ext

added theorem OneHom.ext_iff

added def OneHom.id

added theorem OneHom.id_comp

added theorem OneHom.mk_coe

added theorem OneHom.one_apply

added theorem OneHom.one_comp

added structure OneHom

added structure ZeroHom

added theorem coe_invMonoidHom

added theorem injective_iff_map_eq_one'

added theorem injective_iff_map_eq_one

added def invMonoidHom

added theorem invMonoidHom_apply

added theorem map_div'

added theorem map_div

added theorem map_eq_one_iff

added theorem map_inv

added theorem map_mul

added theorem map_mul_eq_one

added theorem map_mul_inv

added theorem map_ne_one_iff

added theorem map_one

added theorem map_pow

added theorem map_zpow'

added theorem map_zpow

added theorem map_zsmul'

added theorem ne_one_of_map

Modified Mathlib/Logic/Nonempty.lean

Modified lean-toolchain