Commit 2023-05-25 08:46 9a3eb6f0

View on Github →

feat: port Algebra.Category.Ring.FilteredColimits (#4305)

Estimated changes

Modified Mathlib.lean

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

added def CommRingCat.FilteredColimits.colimit

added def CommRingCat.FilteredColimits.colimitCocone

added def CommRingCat.FilteredColimits.colimitCoconeIsColimit

added def CommSemiRingCat.FilteredColimits.colimit

added def CommSemiRingCat.FilteredColimits.colimitCocone

added def CommSemiRingCat.FilteredColimits.colimitCoconeIsColimit

added def RingCat.FilteredColimits.colimit

added def RingCat.FilteredColimits.colimitCocone

added def RingCat.FilteredColimits.colimitCoconeIsColimit

added def SemiRingCat.FilteredColimits.colimit

added def SemiRingCat.FilteredColimits.colimitCocone

added def SemiRingCat.FilteredColimits.colimitCoconeIsColimit