Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-22 16:25 31906d88

View on Github →

chore(algebra/category/CommRing/limits): fix typo, remove private (#1584)

  • chore(algebra/category/CommRing/limits): fix typo, remove private
  • Update src/algebra/category/CommRing/limits.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/algebra/category/CommRing/limits.lean
  • Update src/algebra/category/CommRing/limits.lean
  • bleh
  • Update src/algebra/category/CommRing/limits.lean

Estimated changes