Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-17 06:56 96ea9b99

View on Github →

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

Estimated changes

deleted def opposite.op
deleted theorem opposite.op_inj
deleted theorem opposite.op_unop
deleted def opposite.unop
deleted theorem opposite.unop_inj
deleted theorem opposite.unop_op
deleted def opposite
deleted def category_theory.op
deleted theorem category_theory.op_inj
deleted theorem category_theory.op_unop
deleted theorem category_theory.unop_inj
deleted theorem category_theory.unop_op
added def opposite.op
added theorem opposite.op_inj
added theorem opposite.op_unop
added def opposite.unop
added theorem opposite.unop_inj
added theorem opposite.unop_op