Mathlib Changelog
Changelog
About
Github
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