Mathlib Changelog
v4
Changelog
About
Github
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