Theorem CategoryTheory.LaxMonoidalFunctor.μ_natural

Modification history

2024-01-31 07:01

Mathlib/CategoryTheory/Monoidal/Functor.lean

feat(CategoryTheory/Monoidal): partially setting simp lemmas (#10061) …

Modified CategoryTheory.LaxMonoidalFunctor.μ_natural View on Github →

2024-01-25 06:29

Mathlib/CategoryTheory/Monoidal/Functor.lean

refactor(CategoryTheory/Monoidal): split the naturality condition of monoidal functors (#9988) …

Added CategoryTheory.LaxMonoidalFunctor.μ_natural View on Github →