Def RingCat

Modification history

2024-03-23 07:28

Mathlib/Algebra/Category/Ring/Basic.lean

chore(SemiRingCat/RingCat): make `SemiRingCat` and `RingCat` reducible (#11595) …

Deleted RingCat View on Github →

2023-05-14 01:40

Mathlib/Algebra/Category/Ring/Basic.lean

feat: port Algebra.Category.Ring.Basic (#3901) …

Added RingCat View on Github →