Commit 2025-11-14 17:31 6b6133e9

View on Github →

feat(CategoryTheory): some API for transporting monoidal morphism properties (#31345)

Estimated changes

Modified Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean

added theorem CategoryTheory.MorphismProperty.IsMonoidal.mk'

Modified Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Sites/Monoidal.lean

added theorem CategoryTheory.GrothendieckTopology.W.transport_isMonoidal