mathlib3
feat(algebra/opposites): add some trivial `@[simp]` lemmas
#1508

Merged

feat(algebra/opposites): add some trivial `@[simp]` lemmas #1508

mergify merged 1 commit into master from opposite-lemmas

feat(algebra/opposites): add some trivial `@[simp]` lemmas

b2d644fd

jcommelin approved these changes on 2019-10-05

jcommelin added ready-to-merge

mergify merged 98dbe27a into master 6 years ago

mergify deleted the opposite-lemmas branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone