to_additive): map_namespace should make a meta constant
#1409

Merged

chore(algebra/group/to_additive): map_namespace should make a meta constant #1409

mergify merged 5 commits into master from ChrisHughes24-patch-3

chore(algebra/group/to_additive): map_namespace should make a meta co…

d3b307d7

ChrisHughes24 requested a review 6 years ago

Update to_additive.lean

6c5c60f1

Update to_additive.lean

556fc48f

robertylewis approved these changes on 2019-09-10

robertylewis added ready-to-merge

Merge branch 'master' into ChrisHughes24-patch-3

b25cde56

Merge branch 'master' into ChrisHughes24-patch-3

81945b7c

mergify merged 8e46fa5a into master 6 years ago

mergify deleted the ChrisHughes24-patch-3 branch 6 years ago

Reviewers

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone