Commit 2024-05-10 20:21 21349deb

View on Github →

feat: comonoid objects are monoid objects in the opposite category (#10094)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

added def Comon_.Comon_equiv_Mon_op_op

added def Comon_.Comon_to_Mon_op_op

added def Comon_.Comon_to_Mon_op_op_obj

added def Comon_.Mon_op_op_to_Comon

added def Comon_.Mon_op_op_to_Comon_obj

Modified Mathlib/CategoryTheory/Monoidal/Opposite.lean

added theorem CategoryTheory.op_tensor_op

added theorem CategoryTheory.unop_tensor_unop