Commit 2023-04-19 11:37 aea85a21

View on Github →

feat: port CategoryTheory.Preadditive.Opposite (#3505)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/Opposite.lean

added def CategoryTheory.opHom

added theorem CategoryTheory.op_add

added theorem CategoryTheory.op_neg

added theorem CategoryTheory.op_sum

added theorem CategoryTheory.op_zero

added theorem CategoryTheory.op_zsmul

added def CategoryTheory.unopHom

added theorem CategoryTheory.unop_add

added theorem CategoryTheory.unop_neg

added theorem CategoryTheory.unop_sum

added theorem CategoryTheory.unop_zero

added theorem CategoryTheory.unop_zsmul