Commit 2020-03-14 23:31 54339730

View on Github →

feat(category_theory): limits and colimits in Ab (#2097)

  • limits and colimits in AddCommGroup
  • feat(category_theory): limits and colimits in Ab
  • to_additive comes last
  • add to nolints
  • Update src/algebra/category/Group/limits.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • docstrings
  • use bundled homs throughout
  • comment about better model of colimits
  • fix comments
  • fixes
  • linter

Estimated changes