Commit 2025-09-17 01:02 35360ac2

View on Github →

feat(CategoryTheory/Monoidal): more natural constructors for monoidal functors (#29564)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Multifunctor.lean

added def CategoryTheory.Functor.LaxMonoidal.CoreMonoidal.ofBifunctor

added def CategoryTheory.Functor.LaxMonoidal.Monoidal.ofBifunctor

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.bottomMapᵣ

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.bottomMapₗ

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap₁

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap₂

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.firstMap₃

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.leftMapᵣ

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.leftMapₗ

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap₁

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap₂

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.secondMap₃

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.topMapᵣ

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor.topMapₗ

added def CategoryTheory.Functor.LaxMonoidal.OplaxMonoidal.ofBifunctor

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₂

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₃

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₁

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₂

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap₃

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ

added def CategoryTheory.Functor.LaxMonoidal.ofBifunctor