Commit 2022-12-16 10:09 75f8cb46

View on Github →

feat: port algebra.hom.group_instances (#941) ~~Todo: to_additive on the CommGroup instance seems to take forever and still not work.~~

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Algebra/Hom/Group.lean

Created Mathlib/Algebra/Hom/GroupInstances.lean

added theorem AddMonoid.End.int_cast_apply

added def AddMonoid.End.mulLeft

added def AddMonoid.End.mulRight

added theorem AddMonoid.End.natCast_apply

added theorem AddMonoidHom.coe_flip_mul

added theorem AddMonoidHom.coe_mul

added theorem AddMonoidHom.map_mul_iff

added def AddMonoidHom.mul

added theorem AddMonoidHom.mul_apply

added def MonoidHom.compHom'

added def MonoidHom.compHom

added def MonoidHom.compl₂

added theorem MonoidHom.compl₂_apply

added def MonoidHom.compr₂

added theorem MonoidHom.compr₂_apply

added def MonoidHom.eval

added theorem MonoidHom.ext_iff₂

added def MonoidHom.flip

added def MonoidHom.flipHom

added theorem MonoidHom.flip_apply

added theorem MonoidHom.map_div₂

added theorem MonoidHom.map_inv₂

added theorem MonoidHom.map_mul₂

added theorem MonoidHom.map_one₂