Commit 2024-01-29 15:34 89f97775

View on Github →

chore: fix Punit->PUnit in CommMon_ (#10089)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

added def CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided

added def CommMon_.EquivLaxBraidedFunctorPUnit.counitIso

added def CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon

added def CommMon_.EquivLaxBraidedFunctorPUnit.unitIso

deleted def CommMon_.EquivLaxBraidedFunctorPunit.commMonToLaxBraided

deleted def CommMon_.EquivLaxBraidedFunctorPunit.counitIso

deleted def CommMon_.EquivLaxBraidedFunctorPunit.laxBraidedToCommMon

deleted def CommMon_.EquivLaxBraidedFunctorPunit.unitIso

added def CommMon_.equivLaxBraidedFunctorPUnit

deleted def CommMon_.equivLaxBraidedFunctorPunit