functor_category): the functor category from a groupoid to a monoidal closed category is monoidal closed (#15643)

Commit

3 years ago

feat(category_theory/closed/functor_category): the functor category from a groupoid to a monoidal closed category is monoidal closed (#15643) Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>

Author

antoinelab01

Parents

619fd4d5

mathlib3 c0e00a87 - feat(category_theory/closed/functor_category): the functor category from a groupoid to a monoidal closed category is monoidal closed (#15643)

mathlib3
c0e00a87 - feat(category_theory/closed/functor_category): the functor category from a groupoid to a monoidal closed category is monoidal closed (#15643)