Theorem CategoryTheory.Functor.obj.η_def

Modification history

2026-03-26 22:21

Mathlib/CategoryTheory/Monoidal/Mon_.lean

feat(CategoryTheory/Monoidal): use `to_additive` for monoid objects (#37167) …

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

2025-04-10 22:03

Mathlib/CategoryTheory/Monoidal/Mon_.lean

feat: if `F` is fully faithful, then so is `F.mapMon` (#23874) …

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