Theorem CategoryTheory.Functor.Monoidal.map_associator_inv'

Modification history

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