Def category_theory.monoidal.transported

Modification history

2020-09-22 11:28

src/category_theory/monoidal/transport.lean

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

Added category_theory.monoidal.transported View on Github →