Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-19 08:46 4bc32ae4

View on Github →

feat(category_theory): regular monos (#2154)

  • feat(category_theory): regular and normal monos
  • fixes
  • Apply suggestions from code review Co-Authored-By: Markus Himmel [email protected]
  • shorter proofs
  • typos, thanks Co-Authored-By: Markus Himmel [email protected]
  • Update src/category_theory/limits/shapes/regular_mono.lean Co-Authored-By: Markus Himmel [email protected]
  • linting

Estimated changes