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 scott@tqft.net
- 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]