Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-29 11:22 5adeebf1

View on Github →

feat(algebra/group/hom): bundled monoid and group homs (#1271)

  • feat(algebra/group/hom): adding bundled group homs
  • adding module docstring
  • moving some group stuff into monoid
  • responding to PR comments
  • mk'' -> mk'
  • spaces before }
  • Update src/algebra/group/hom.lean
  • Update src/algebra/group/hom.lean
  • Update src/algebra/group/hom.lean
  • Update src/algebra/group/hom.lean
  • Update hom.lean

Estimated changes

added theorem add_monoid_hom.map_neg
added theorem add_monoid_hom.map_sub
added structure add_monoid_hom
added def monoid_hom.comp
added def monoid_hom.ext
added def monoid_hom.id
added theorem monoid_hom.map_div
added theorem monoid_hom.map_inv
added theorem monoid_hom.map_mul
added theorem monoid_hom.map_one
added def monoid_hom.mk'
added structure monoid_hom