Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-04-09 17:28
6abb6de9
View on Github →
feat(category_theory/bicategory): monoidal categories are single object bicategories (
#13157
)
Estimated changes
Created
src/category_theory/bicategory/End.lean
added
def
category_theory.End_monoidal
Modified
src/category_theory/bicategory/basic.lean
Created
src/category_theory/bicategory/single_obj.lean
added
def
category_theory.monoidal_single_obj.End_monoidal_star_functor
added
def
category_theory.monoidal_single_obj.End_monoidal_star_functor_is_equivalence
added
def
category_theory.monoidal_single_obj