Theorem CategoryTheory.Functor.LaxMonoidal.tensorHom_ε_comp_μ

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.LaxMonoidal.tensorHom_ε_comp_μView on Github →