Commit 2024-02-16 21:36 09342771

View on Github →

Refactor(Mathlib/CategoryTheory/Monoidal/Opposite): Make MonoidalOpposite a structure (#10642) Refactor MonoidalOpposite into a structure for consistency with Opposite.

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Opposite.lean

modified def CategoryTheory.Iso.mop

modified def CategoryTheory.Iso.unmop

deleted def CategoryTheory.MonoidalOpposite.mop

added def CategoryTheory.MonoidalOpposite.mopEquiv

modified def CategoryTheory.MonoidalOpposite.mopMopEquivalence

modified theorem CategoryTheory.MonoidalOpposite.mop_inj_iff

modified theorem CategoryTheory.MonoidalOpposite.mop_injective

modified theorem CategoryTheory.MonoidalOpposite.mop_unmop

deleted def CategoryTheory.MonoidalOpposite.underlyingEquiv

deleted def CategoryTheory.MonoidalOpposite.unmop

added def CategoryTheory.MonoidalOpposite.unmopEquiv

modified theorem CategoryTheory.MonoidalOpposite.unmop_inj_iff

modified theorem CategoryTheory.MonoidalOpposite.unmop_mop

added structure CategoryTheory.MonoidalOpposite

deleted def CategoryTheory.MonoidalOpposite

modified def CategoryTheory.mopFunctor

modified theorem CategoryTheory.mop_comp

modified theorem CategoryTheory.mop_id

modified theorem CategoryTheory.mop_id_unmop

modified def CategoryTheory.unmopFunctor

modified theorem CategoryTheory.unmop_comp

modified theorem CategoryTheory.unmop_id

modified theorem CategoryTheory.unmop_id_mop

modified def Quiver.Hom.mop

modified def Quiver.Hom.unmop