`
#2056

Merged

chore(algebra/group): move `is_mul/monoid/group_hom` to `deprecated/` #2056

mergify merged 8 commits into master from hom-deprecate

Move `is_mul/monoid/group_hom` to `deprecated/`

ed42b2cc

chore(algebra/group): move `is_mul/monoid/group_hom` to `deprecated/`

ad9d055a

Adjust module docstring

c5fd1721

urkud added awaiting-review

kim-em approved these changes on 2020-02-28

kim-em added ready-to-merge

kim-em removed awaiting-review

Merge branch 'master' into hom-deprecate

f8626170

Merge branch 'master' into hom-deprecate

475f1366

urkud commented on 2020-03-01

Update src/algebra/group/with_one.lean

0452f76f

Merge branch 'master' into hom-deprecate

7b7a2849

Merge branch 'master' into hom-deprecate

d9d94e30

mergify merged bfbd0937 into master 5 years ago

mergify deleted the hom-deprecate branch 5 years ago

Reviewers

kim-em

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone