Theorem CategoryTheory.GrothendieckTopology.W.transport_isMonoidal

Modification history

2025-11-14 17:31
Mathlib/CategoryTheory/Sites/Monoidal.lean
feat(CategoryTheory): some API for transporting monoidal morphism properties (#31345)
Added CategoryTheory.GrothendieckTopology.W.transport_isMonoidalView on Github →