PR #538 feat(algebra/opposites): opposites of operators

feat(algebra/opposites): opposites of operators #538

rwbarton merged 7 commits into leanprover-community:master from leanprover-fork:opposites

digama0 commented on 2018-12-21

kckennylau force pushed from 3a4afad3 to 69f79824 6 years ago

kckennylau force pushed from 69f79824 to b55799ff 6 years ago

johoelzl changed the title ~~feat(algebra/opposites) opposites~~ feat(algebra/opposites): opposites of operators 6 years ago

feat(algebra/opposites): opposites

e1352cae

feat(algebra/opposites): make opposite inductive

f918b496

refactor(algebra/opposites): move into src

e3e783fe

kckennylau force pushed from 89207507 to e3e783fe 6 years ago

feat(algebra/opposites): make opposite semireducible

7aad9a05

cipher1024 assigned

digama0 6 years ago

Merge branch 'master' into opposites

70154544

cipher1024 force-pushed the master branch from 1ed7ad11 to f623d346 6 years ago

cipher1024 force-pushed the master branch from f623d346 to 1ed7ad11 6 years ago

Merge branch 'master' into opposites

ecb9e71f

rwbarton approved these changes on 2019-04-05

rwbarton added ready-to-merge

Merge branch 'master' into 'opposites'

cc4e2607

kckennylau requested a review 6 years ago

rwbarton merged d8a2bc51 into master 6 years ago

Reviewers

rwbarton

digama0

Assignees

digama0

Labels

ready-to-merge

Milestone

No milestone