Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-20 18:35 0ab8a89d

View on Github →

feat(category_theory): limits in CommRing (#1006)

feat(category_theory): limits in CommRing
by
rename
sections
Update src/category_theory/types.lean Co-Authored-By: Johannes Hölzl johannes.hoelzl@gmx.de

Estimated changes

Modified src/algebra/pi_instances.lean

deleted def pi.is_ring_hom_pi

Modified src/category_theory/instances/CommRing/basic.lean

Created src/category_theory/instances/CommRing/limits.lean

added def category_theory.instances.CommRing.limit

added def category_theory.instances.CommRing.limit_is_limit

Modified src/category_theory/limits/types.lean

Modified src/category_theory/types.lean

added def category_theory.functor.sections