Def RingEquiv.piEquivPi

Modification history

2025-08-08 10:25

Mathlib/Algebra/Category/Ring/Constructions.lean

chore: remove `suppress_compilation` from Mathlib.Algebra.Category.Ring.Constructions (#27248)

Deleted RingEquiv.piEquivPi View on Github →

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 RingEquiv.piEquivPi View on Github →