Def SemiRingCat.forget₂AddCommMonPreservesLimitsAux

Modification history

2024-03-24 13:55

Mathlib/Algebra/Category/Ring/Limits.lean

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

Modified SemiRingCat.forget₂AddCommMonPreservesLimitsAux View on Github →

2023-05-25 17:58

Mathlib/Algebra/Category/Ring/Limits.lean

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

Added SemiRingCat.forget₂AddCommMonPreservesLimitsAux View on Github →