Commit 2025-05-10 22:55 a55bbf79

View on Github →

refactor: generalise the equivalence Comon_ C ≌ C to an arbitrary MonoidalCategory instance (#24729) ... instead of the one coming from arbitrary choices. From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean

deleted theorem comul_eq_diag

added theorem comul_eq_lift

deleted theorem counit_eq_from

added theorem counit_eq_toUnit