Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-28 14:47 052447d3

View on Github →

feat(algebra/group/hom_instance): add add_monoid_hom.mul (#7382)

Estimated changes

Modified src/algebra/group/hom_instances.lean

added theorem add_monoid_hom.coe_flip_mul

added theorem add_monoid_hom.coe_mul

added def add_monoid_hom.mul

added theorem add_monoid_hom.mul_apply