Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-07 15:39 03dd404a

View on Github →

feat(algebra/category): (co)limits in CommRing (#10593)

Estimated changes

Created src/algebra/category/CommRing/constructions.lean

added def CommRing.Z_is_initial

added def CommRing.equalizer_fork

added def CommRing.equalizer_fork_is_limit

added def CommRing.prod_fan

added def CommRing.prod_fan_is_limit

added def CommRing.punit_is_terminal

added def CommRing.pushout_cocone

added theorem CommRing.pushout_cocone_X

added theorem CommRing.pushout_cocone_inl

added theorem CommRing.pushout_cocone_inr

added def CommRing.pushout_cocone_is_colimit

Deleted src/algebra/category/CommRing/pushout.lean

deleted def CommRing.pushout_cocone

deleted theorem CommRing.pushout_cocone_X

deleted theorem CommRing.pushout_cocone_inl

deleted theorem CommRing.pushout_cocone_inr

deleted def CommRing.pushout_cocone_is_colimit

Modified src/ring_theory/ideal/local_ring.lean