Commit 2025-12-03 14:57 8198848b

View on Github →

chore: generalize Subring.toIsOrderedRing to SubringClass (#32212)

Estimated changes

Modified Mathlib/Algebra/Ring/Subring/Order.lean

modified def Subring.orderedSubtype