Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-11 10:12 86d0f292

View on Github →

refactor(*): make is_group_hom extend is_mul_hom (#1214)

  • map_mul/map_add: use explicit parameters Preparing to merge is_mul_hom with is_group_hom
  • make is_group_hom extend is_mul_hom, adjust many proof terms
  • Add a comment

Estimated changes

modified theorem is_add_monoid_hom.map_add
modified theorem is_group_hom.inv
added theorem is_group_hom.mk'
modified theorem is_group_hom.mul
modified theorem is_monoid_hom.map_mul
deleted theorem is_mul_hom.comp'
deleted theorem is_mul_hom.comp
deleted theorem is_mul_hom.id
added theorem is_mul_hom.inv
added theorem is_mul_hom.mul
deleted theorem units.map_comp'