Commit 2025-05-22 22:11 b057c67c

View on Github →

feat(CategoryTheory/Monoidal): replace Mon_ lemmas with Mon_Class lemmas (#24597) extracted from #15254

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

deleted theorem CategoryTheory.Equivalence.Mon_.Mon_tensor_mul_assoc

deleted theorem CategoryTheory.Equivalence.Mon_.Mon_tensor_mul_one

deleted theorem CategoryTheory.Equivalence.Mon_.Mon_tensor_one_mul

deleted theorem CategoryTheory.Equivalence.Mon_.mul_associator

deleted theorem CategoryTheory.Equivalence.Mon_.mul_braiding

deleted theorem CategoryTheory.Equivalence.Mon_.mul_leftUnitor

deleted theorem CategoryTheory.Equivalence.Mon_.mul_rightUnitor

deleted theorem CategoryTheory.Equivalence.Mon_.one_associator

deleted theorem CategoryTheory.Equivalence.Mon_.one_braiding

deleted theorem CategoryTheory.Equivalence.Mon_.one_leftUnitor

deleted theorem CategoryTheory.Equivalence.Mon_.one_rightUnitor

added theorem CategoryTheory.Equivalence.Mon_Class.Mon_tensor_mul_assoc

added theorem CategoryTheory.Equivalence.Mon_Class.Mon_tensor_mul_one

added theorem CategoryTheory.Equivalence.Mon_Class.Mon_tensor_one_mul

added theorem CategoryTheory.Equivalence.Mon_Class.mul_associator

added theorem CategoryTheory.Equivalence.Mon_Class.mul_braiding

added theorem CategoryTheory.Equivalence.Mon_Class.mul_leftUnitor

added theorem CategoryTheory.Equivalence.Mon_Class.mul_rightUnitor

added theorem CategoryTheory.Equivalence.Mon_Class.one_associator

added theorem CategoryTheory.Equivalence.Mon_Class.one_braiding

added theorem CategoryTheory.Equivalence.Mon_Class.one_leftUnitor

added theorem CategoryTheory.Equivalence.Mon_Class.one_rightUnitor

added def Mon_.mkIso'

modified def Mon_.trivial