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_η_tensorHomView on Github →