Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-12 13:20 08880c94

View on Github →

feat(data/equiv,category_theory): prove equivalences are the same as isos (#1587)

  • refactor(category_theory,algebra/category): make algebraic categories not [reducible] Adapted from part of #1438.
  • Update src/algebra/category/CommRing/basic.lean Co-Authored-By: Scott Morrison
  • adding missing forget2 instances
  • Converting Reid's comment to a [Note]
  • adding examples testing coercions
  • feat(data/equiv/algebra): equivalence of algebraic equivalences and categorical isomorphisms
  • more @[simps]
  • more @[simps]

Estimated changes