Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-22 02:29 c9ba7a5c

View on Github →

refactor(category_theory,algebra/category): make algebraic categories not [reducible] (#1491)

  • 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

Estimated changes

deleted theorem CommRing.comp_eq
deleted theorem CommRing.id_eq
modified def CommRing
modified def CommSemiRing
modified def Ring
modified def SemiRing
modified def CommGroup
modified def Group
modified def CommMon.of
modified def CommMon
added theorem category_theory.coe_id