Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-04 12:27 8cd16b97

View on Github →

feat(category_theory/sums): sums (disjoint unions) of categories (#1357)

  • feat(category_theory/sum): direct sums of categories
  • minor
  • tidying
  • Fix white space, remove old comments
  • rearranging, associator
  • add TODO comment about unitors
  • fix import
  • create /basic.lean files

Estimated changes

deleted theorem category_theory.prod_comp
deleted theorem category_theory.prod_id