Commit 2024-10-18 15:58 94bb3a8e

View on Github →

feat(CategoryTheory/Monoidal): add Mon_Class type class (#17185) Zulip discussion

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Bimon_.lean

added theorem Bimon_Class.mul_comul

added theorem Bimon_Class.mul_counit

added theorem Bimon_Class.one_comul

added theorem Bimon_Class.one_counit

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

added def Comon_.mk'

added theorem Comon_Class.comul_assoc

added theorem Comon_Class.comul_counit

added theorem Comon_Class.counit_comul

Modified Mathlib/CategoryTheory/Monoidal/Hopf_.lean

added theorem Hopf_Class.antipode_left

added theorem Hopf_Class.antipode_right

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

added def Mon_.mk'

added theorem Mon_Class.mul_assoc

added theorem Mon_Class.mul_one

added theorem Mon_Class.one_mul