Commit 2025-09-24 23:34 1d84eb6e

View on Github →

feat: miscellaneous grind golfs (#29700)

Estimated changes

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

Modified Mathlib/Algebra/Polynomial/Derivative.lean

Modified Mathlib/Combinatorics/Matroid/Map.lean

Modified Mathlib/Data/Int/Init.lean

Modified Mathlib/Data/Nat/Bits.lean

modified theorem Nat.binaryRec_decreasing

Modified Mathlib/Data/Nat/Digits/Lemmas.lean

Modified Mathlib/Data/Nat/Size.lean

Modified Mathlib/Data/PEquiv.lean

Modified Mathlib/MeasureTheory/Constructions/Cylinders.lean

Modified Mathlib/MeasureTheory/PiSystem.lean

Modified Mathlib/Order/WellFoundedSet.lean