Theorem CategoryTheory.Functor.Monoidal.inv_η

Modification history

2025-07-14 16:30
Mathlib/CategoryTheory/Monoidal/Functor.lean
feat(CategoryTheory): `inv (μ F X Y) = δ F X Y` (#27061) …
Added CategoryTheory.Functor.Monoidal.inv_ηView on Github →