Def CommRingCat.piFanIsLimit

Modification history

2024-02-14 03:21

Mathlib/Algebra/Category/Ring/Constructions.lean

feat(Algebra/Category/Ring/Constructions): categorical product of rings is the cartesian product (#9394)

Added CommRingCat.piFanIsLimit View on Github →