Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-25 17:58
e53aed11
View on Github →
feat: port Algebra.Category.Ring.Limits (
#4235
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Category/Ring/Basic.lean
added
def
RingEquiv.toCommSemiRingCatIso
added
def
RingEquiv.toSemiRingCatIso
Modified
Mathlib/Algebra/Category/Ring/FilteredColimits.lean
Created
Mathlib/Algebra/Category/Ring/Limits.lean
added
def
CommRingCat.forget₂CommSemiRingPreservesLimitsAux
added
def
CommRingCat.limitCone
added
def
CommRingCat.limitConeIsLimit
added
def
CommSemiRingCat.limitCone
added
def
CommSemiRingCat.limitConeIsLimit
added
def
RingCat.forget₂AddCommGroupPreservesLimitsAux
added
def
RingCat.limitCone
added
def
RingCat.limitConeIsLimit
added
def
RingCat.sectionsSubring
added
def
SemiRingCat.HasLimits.limitCone
added
def
SemiRingCat.HasLimits.limitConeIsLimit
added
def
SemiRingCat.forget₂AddCommMonPreservesLimitsAux
added
def
SemiRingCat.forget₂MonPreservesLimitsAux
added
def
SemiRingCat.limitπRingHom
added
def
SemiRingCat.sectionsSubsemiring