Theorem CategoryTheory.Functor.obj.ε_def

Modification history

2025-09-13 17:38

Mathlib/CategoryTheory/Monoidal/Comon_.lean

chore: rename `Mon_Class` to `MonObj` (#28406) …

Modified CategoryTheory.Functor.obj.ε_def View on Github →

2025-06-15 16:58

Mathlib/CategoryTheory/Monoidal/Comon_.lean

refactor(CategoryTheory/Monoidal): define `Mon_.Hom` using type class `IsMon_Hom` (#25826) …

Added CategoryTheory.Functor.obj.ε_def View on Github →