Commit 2023-05-26 05:11 ca45801a

View on Github →

feat: port Algebra.Category.Ring.Constructions (#4366)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/Ring/Constructions.lean

added def CommRingCat.equalizerFork

added def CommRingCat.equalizerForkIsLimit

added def CommRingCat.prodFan

added def CommRingCat.prodFanIsLimit

added def CommRingCat.pullbackCone

added def CommRingCat.pullbackConeIsLimit

added def CommRingCat.punitIsTerminal

added def CommRingCat.pushoutCocone

added def CommRingCat.pushoutCoconeIsColimit

added theorem CommRingCat.pushoutCocone_inl

added theorem CommRingCat.pushoutCocone_inr

added theorem CommRingCat.pushoutCocone_pt

added theorem CommRingCat.subsingleton_of_isTerminal

added def CommRingCat.zIsInitial