Theorem Comon_.tensorObj_comul

Modification history

2025-06-04 18:15
Mathlib/CategoryTheory/Monoidal/Comon_.lean
feat(CategoryTheory/Monoidal): define Mon_ by using Mon_Class (#24646) …
Modified Comon_.tensorObj_comulView on Github →
2024-05-23 18:22
Mathlib/CategoryTheory/Monoidal/Comon_.lean
feat: comonoid objects in a braided category form a monoidal category (#10098)
Added Comon_.tensorObj_comulView on Github →