group`
#2060

Merged

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

mergify merged 6 commits into master from free-monoid

Move `free_monoid` from `algebra/group/` to `algebra/`

e62e27c0

feat(algebra/free_monoid): define `lift` and `map`

f9af4d23

Expand docstring, drop unneeded arguments to `to_additive`

3fece164

Fix compile

e3344f2e

urkud changed the title ~~feat(algebra/free_monoid): define `lift` and `map`~~ feat(algebra/free_monoid): define `lift` and `map`, move out of `algebra/group` 5 years ago

urkud added awaiting-review

sgouezel commented on 2020-03-01

Update src/algebra/free_monoid.lean

04b9f326

sgouezel approved these changes on 2020-03-01

sgouezel removed awaiting-review

sgouezel added ready-to-merge

Merge branch 'master' into free-monoid

134a3e9e

mergify merged d5d907b1 into master 5 years ago

mergify deleted the free-monoid branch 5 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone

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

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

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

Merged