Commit 2026-03-26 12:09 13476e26

View on Github →

chore: use inferInstanceAs in WithTop file (#37124)

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

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

Modified Mathlib/Algebra/Order/SuccPred/WithBot.lean

modified theorem WithBot.succ_one

modified theorem WithBot.succ_zero

Modified Mathlib/Order/WithBot.lean