Commit 2025-02-07 21:32 1aa7ca01

View on Github →

feat(CategoryTheory): the forgetful functor from CommMon_ C to C (#21553)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

added def CommMon_.forget

added theorem CommMon_.forget₂Mon_comp_forget

added theorem CommMon_.forget₂Mon_map_hom

added theorem CommMon_.forget₂Mon_obj_mul

added theorem CommMon_.forget₂Mon_obj_one

deleted theorem CommMon_.forget₂_Mon_map_hom

deleted theorem CommMon_.forget₂_Mon_obj_mul

deleted theorem CommMon_.forget₂_Mon_obj_one