Def category_theory.monoidal.transported_monoidal_unit_iso

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_monoidal_unit_iso View on Github →