Theorem CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_ε

Modification history

2025-11-18 16:33
Mathlib/CategoryTheory/Localization/Monoidal/Functor.lean
feat(CategoryTheory): the universal property of localized monoidal categories (#25799) …
Added CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_εView on Github →