Commit 2023-06-14 07:51 d7461044

View on Github →

feat: port CategoryTheory.Monoidal.CommMon_ (#5012)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided.lean

added theorem CategoryTheory.BraidedFunctor.ext'

added theorem CategoryTheory.LaxBraidedFunctor.ext'

Created Mathlib/CategoryTheory/Monoidal/CommMon_.lean

added def CategoryTheory.LaxBraidedFunctor.mapCommMon

added def CategoryTheory.LaxBraidedFunctor.mapCommMonFunctor

added def CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided

added def CommMon_.EquivLaxBraidedFunctorPunit.counitIso

added def CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon

added def CommMon_.EquivLaxBraidedFunctorPunit.unitIso

added theorem CommMon_.comp'

added theorem CommMon_.comp_hom

added def CommMon_.equivLaxBraidedFunctorPunit

added def CommMon_.forget₂Mon_

added theorem CommMon_.forget₂_Mon_map_hom

added theorem CommMon_.forget₂_Mon_obj_mul

added theorem CommMon_.forget₂_Mon_obj_one

added theorem CommMon_.hom_ext

added theorem CommMon_.id'

added theorem CommMon_.id_hom

added def CommMon_.trivial

added structure CommMon_