mathlib

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

chore(opposites): merge two definitions of `opposite` (#1036) * chore(opposites): merge two definitions of `opposite` * merge `opposite.opposite` from `algebra/opposites` with `category_theory.opposite` from `category_theory/opposites`, and put it into `data/opposite` * main reasons: DRY, avoid confusion if both namespaces are open * see https://github.com/leanprover-community/mathlib/pull/538#issuecomment-459488227 * Authors merged from `git blame` output on both original files; I assume my contribution to be trivial * Update opposite.lean