mathlib

d09ef4ab - feat(category_theory/monoidal): transport monoidal structure along an equivalence (#4123)