Commit 2022-12-13 13:20 dd4f8930

View on Github →

feat: port Algebra.Group.Prod (#968) mathlib3 SHA: cf9386b56953fb40904843af98b7a80757bbe7f9

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Group/Prod.lean

added theorem MonoidHom.coe_fst

added theorem MonoidHom.coe_prod

added theorem MonoidHom.coe_prodMap

added theorem MonoidHom.coe_snd

added theorem MonoidHom.comp_coprod

added def MonoidHom.coprod

added theorem MonoidHom.coprod_apply

added theorem MonoidHom.coprod_comp_inl

added theorem MonoidHom.coprod_comp_inr

added theorem MonoidHom.coprod_inl_inr

added theorem MonoidHom.coprod_unique

added def MonoidHom.fst

added theorem MonoidHom.fst_comp_inl

added theorem MonoidHom.fst_comp_inr

added theorem MonoidHom.fst_comp_prod

added def MonoidHom.inl

added theorem MonoidHom.inl_apply

added def MonoidHom.inr

added theorem MonoidHom.inr_apply

added def MonoidHom.prodMap

added theorem MonoidHom.prodMap_def

added theorem MonoidHom.prod_apply

added theorem MonoidHom.prod_comp_prodMap

added theorem MonoidHom.prod_unique

added def MonoidHom.snd

added theorem MonoidHom.snd_comp_inl

added theorem MonoidHom.snd_comp_inr

added theorem MonoidHom.snd_comp_prod

added theorem MulEquiv.coe_prodComm

added theorem MulEquiv.coe_prodComm_symm

added def MulEquiv.prodComm

added def MulEquiv.prodCongr

added def MulEquiv.prodUnique

added def MulEquiv.prodUnits

added def MulEquiv.uniqueProd

added theorem MulHom.coe_fst

added theorem MulHom.coe_prod

added theorem MulHom.coe_prodMap

added theorem MulHom.coe_snd

added theorem MulHom.comp_coprod

added def MulHom.coprod

added theorem MulHom.coprod_apply

added def MulHom.fst

added theorem MulHom.fst_comp_prod

added def MulHom.prodMap

added theorem MulHom.prodMap_def

added theorem MulHom.prod_apply

added theorem MulHom.prod_comp_prodMap

added theorem MulHom.prod_unique

added def MulHom.snd

added theorem MulHom.snd_comp_prod

added theorem Prod.fst_div

added theorem Prod.fst_inv

added theorem Prod.fst_mul

added theorem Prod.fst_mul_snd

added theorem Prod.fst_one

added theorem Prod.inv_mk

added theorem Prod.mk_div_mk

added theorem Prod.mk_eq_one

added theorem Prod.mk_mul_mk

added theorem Prod.mk_one_mul_mk_one

added theorem Prod.mul_def

added theorem Prod.one_eq_mk

added theorem Prod.one_mk_mul_one_mk

added theorem Prod.snd_div

added theorem Prod.snd_inv

added theorem Prod.snd_mul

added theorem Prod.snd_one

added theorem Prod.swap_div

added theorem Prod.swap_inv

added theorem Prod.swap_mul

added theorem Prod.swap_one

added def Units.embedProduct

added theorem Units.embedProduct_injective

added def divMonoidHom

added def divMonoidWithZeroHom

added def mulMonoidHom

added def mulMonoidWithZeroHom

added def mulMulHom