mathlib3
feat(algebra/group): conversion between `→*` and `→+`
#1569

Merged

feat(algebra/group): conversion between `→*` and `→+` #1569

mergify merged 5 commits into master from mult-monoid-hom

feat(algebra/group): conversion between `→*` and `→+`

10879d84

docs

9bcb5fe8

jcommelin commented on 2019-10-19

Rename to allow use of projection notation

70e57cb5

Merge branch 'master' into mult-monoid-hom

31e1c8c8

kim-em approved these changes on 2019-10-22

jcommelin added ready-to-merge

Merge branch 'master' into mult-monoid-hom

84d6090d

mergify merged e8bdb05e into master 6 years ago

mergify deleted the mult-monoid-hom branch 6 years ago

Reviewers

kim-em

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone