Def category_theory.monoidal_single_obj.End_monoidal_star_functor_is_equivalence

Modification history

2022-04-09 17:28
src/category_theory/bicategory/single_obj.lean
feat(category_theory/bicategory): monoidal categories are single object bicategories (#13157)
Added category_theory.monoidal_single_obj.End_monoidal_star_functor_is_equivalenceView on Github →