Commit 2020-09-12 09:38 88dd01b7

View on Github →

chore(category_theory): minor cleanups (#4110)

Estimated changes

Modified src/algebra/category/Group/colimits.lean

added def AddCommGroup.colimits.colimit_cocone_is_colimit

deleted def AddCommGroup.colimits.colimit_is_colimit

Modified src/category_theory/limits/limits.lean

added def category_theory.limits.is_colimit.map

deleted def category_theory.limits.is_colimit_map

added def category_theory.limits.is_limit.map

deleted def category_theory.limits.is_limit_map

Modified src/category_theory/limits/shapes/biproducts.lean

Modified src/category_theory/types.lean

added theorem category_theory.hom_inv_id_apply

added theorem category_theory.inv_hom_id_apply