Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-04 11:10 e1b1d17a

View on Github →

feat(algebra/group): construct add_monoid_hom from map_sub (#4382)

Estimated changes

Modified src/algebra/group/hom.lean

added theorem add_monoid_hom.coe_of_map_sub

modified theorem add_monoid_hom.map_sub

added def add_monoid_hom.of_map_sub

added theorem monoid_hom.coe_of_map_mul_inv

added def monoid_hom.of_map_mul_inv