Commit 2023-06-08 08:49 3dbd9bf3

View on Github →

feat: port CategoryTheory.Monoidal.Opposite (#4850)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Opposite.lean

added def CategoryTheory.Iso.mop

added def CategoryTheory.MonoidalOpposite.mop

added theorem CategoryTheory.MonoidalOpposite.mop_unmop

added theorem CategoryTheory.MonoidalOpposite.op_inj_iff

added theorem CategoryTheory.MonoidalOpposite.op_injective

added def CategoryTheory.MonoidalOpposite.unmop

added theorem CategoryTheory.MonoidalOpposite.unmop_mop

added theorem CategoryTheory.MonoidalOpposite.unop_inj_iff

added theorem CategoryTheory.MonoidalOpposite.unop_injective

added def CategoryTheory.MonoidalOpposite

added theorem CategoryTheory.mop_comp

added theorem CategoryTheory.mop_id

added theorem CategoryTheory.mop_id_unmop

added theorem CategoryTheory.mop_inj

added theorem CategoryTheory.mop_tensorObj

added theorem CategoryTheory.mop_tensorUnit

added theorem CategoryTheory.mop_unmop

added theorem CategoryTheory.op_tensorObj

added theorem CategoryTheory.op_tensorUnit

added theorem CategoryTheory.unmop_comp

added theorem CategoryTheory.unmop_id

added theorem CategoryTheory.unmop_id_mop

added theorem CategoryTheory.unmop_inj

added theorem CategoryTheory.unmop_mop

added def Quiver.Hom.mop

added def Quiver.Hom.unmop