Def CommRingCat.piIsoPi

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 CommRingCat.piIsoPiView on Github →
2024-05-27 10:06
Mathlib/Algebra/Category/Ring/Constructions.lean
style: change the notation for `CategoryTheory.Limits.piObj` from `∏ f` to `∏ᶜ f` (#13269) …
Modified CommRingCat.piIsoPiView 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 CommRingCat.piIsoPiView on Github →