Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-02 08:53 d5d907b1

View on Github →

feat(algebra/free_monoid): define lift and map, move out of algebra/group (#2060)

  • Move free_monoid from algebra/group/ to algebra/
  • feat(algebra/free_monoid): define lift and map
  • Expand docstring, drop unneeded arguments to to_additive
  • Fix compile
  • Update src/algebra/free_monoid.lean Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr

Estimated changes

added theorem free_monoid.hom_eq
added def free_monoid.lift
added def free_monoid.map
added theorem free_monoid.map_comp
added theorem free_monoid.map_of
added theorem free_monoid.mul_def
added def free_monoid.of
added theorem free_monoid.one_def
added def free_monoid
deleted theorem free_monoid.mul_def
deleted theorem free_monoid.one_def
deleted def free_monoid