mathlib3
chore(opposites): merge two definitions of `opposite`
#1036

Merged

chore(opposites): merge two definitions of `opposite` #1036

mergify merged 3 commits into leanprover-community:master from urkud:merge-opposite

chore(opposites): merge two definitions of `opposite`

50effcb4

urkud requested a review 6 years ago

Merge branch 'master' into merge-opposite

3f217d45

Update opposite.lean

89b22c31

jcommelin approved these changes on 2019-05-17

jcommelin added ready-to-merge

mergify merged 96ea9b99 into master 6 years ago

urkud deleted the merge-opposite branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone