Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-16 06:42 28959d93

View on Github →

feat(category_theory/closed/monoidal): transport monoidal_closed across a monoidal equivalence (#15530)

Estimated changes

Modified src/category_theory/closed/monoidal.lean

added def category_theory.monoidal_closed.of_equiv

Created src/category_theory/functor/inv_isos.lean

added def category_theory.comp_inv_iso

added def category_theory.inv_comp_iso

added def category_theory.iso_comp_inv

added def category_theory.iso_inv_comp

Modified src/category_theory/monoidal/functor.lean