PR #1345 refactor(*): rewrite `to_additive` attribute

refactor(*): rewrite `to_additive` attribute #1345

mergify merged 14 commits into leanprover-community:master from urkud:to_additive

chore(algebra/group/to_additive): auto add structure fields

6e2acb3a

Snapshot

d2546d86

Rewrite `@[to_additive]`

37b15d4e

urkud requested a review 6 years ago

Drop more explicit `name` arguments to `to_additive`

438507e0

Drop more explicit arguments to `to_additive`

0121f93e

Merge branch 'master' into to_additive, resolve conflicts

675b5cbc

Map namespaces with `run_cmd to_additive.map_namespace`

9b942240

fix(`group_theory/perm/sign`): fix compile

2f912762

Fix handling of equational lemmas; fix warnings

f3ff755d

khoek commented on 2019-08-19

Use `list.mmap'`

57d3feab

Merge branch 'master' into to_additive

5a9d0175

Merge branch 'master' into to_additive

76973a2c

Merge branch 'master' into to_additive

8d38e172

cipher1024 approved these changes on 2019-08-21

cipher1024 added ready-to-merge

Merge branch 'master' into to_additive

d1e9285c

mergify merged c5128756 into master 6 years ago

urkud deleted the to_additive branch 6 years ago

Reviewers

cipher1024

khoek

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone