with_one`
#1227

Merged

refactor(algebra/*): delete `free_monoid` from `algebra/free`, restore some functions in `algebra/group/with_one` #1227

mergify merged 9 commits into leanprover-community:master from urkud:free-monoid

refactor(algebra/*): Remove `free_monoid` from `algebra/free`, fixes …

a9fa9474

use `namespace with_one`

5e01ba23

Add `with_one.coe_is_mul_hom`

42344ed0

Restore `with_one.lift` etc from `algebra/free` `free_monoid.lift` etc

894c23b9

Define `with_one.map` based on the deleted `free_monoid.map`

581be7fc

urkud requested a review 6 years ago

Merge branch 'master' into free-monoid

b327c144

Merge branch 'master' into free-monoid

dfd38743

Merge branch 'master' into free-monoid

3b314ff9

jcommelin approved these changes on 2019-07-19

jcommelin added ready-to-merge

Merge branch 'master' into free-monoid

c13bb5f0

mergify merged 07ae80f4 into master 6 years ago

urkud deleted the free-monoid branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone