Commit 2025-08-08 10:25 63b8cd5a

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

deleted def CommRingCat.piIsoPi

deleted def RingEquiv.piEquivPi