Theorem CategoryTheory.Functor.OplaxMonoidal.δ_comp_tensorHom_η

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.OplaxMonoidal.δ_comp_tensorHom_ηView on Github →