Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-10 02:08 86bd577c

View on Github →

refactor(algebra/group): is_monoid_hom extends is_mul_hom (#915)

refactor(algebra/group): is_monoid_hom extends is_mul_hom
Fix build

Estimated changes

Modified src/algebra/group.lean

added theorem is_add_monoid_hom.map_add

added theorem is_monoid_hom.map_mul

Modified src/algebra/group_power.lean

Modified src/algebra/module.lean

Modified src/algebra/pi_instances.lean

Modified src/algebra/punit_instances.lean

Modified src/analysis/normed_space/basic.lean

Modified src/category/fold.lean

Modified src/data/dfinsupp.lean

Modified src/data/finsupp.lean

Modified src/data/matrix.lean

Modified src/data/multiset.lean

Modified src/data/nat/cast.lean

Modified src/data/polynomial.lean