Mathlib v3 is deprecated. Go to Mathlib v4

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

added def Ab
added theorem CommGroup.one_apply
added theorem Group.one_apply