mathlib3

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

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> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>