Def CommRingCat.forget₂CommSemiRingPreservesLimitsAux

Modification history

2024-03-24 13:55

Mathlib/Algebra/Category/Ring/Limits.lean

refactor(Algebra/Category): replace `TypeMax` constructions by `UnivLE` assumptions (#11420) …

Modified CommRingCat.forget₂CommSemiRingPreservesLimitsAux View on Github →

2023-05-25 17:58

Mathlib/Algebra/Category/Ring/Limits.lean

feat: port Algebra.Category.Ring.Limits (#4235)

Added CommRingCat.forget₂CommSemiRingPreservesLimitsAux View on Github →