Commit 2026-07-24 12:28 014cbc3f

View on Github →

fix(Order/Partition): rename a binder shadowing Partition.sSup_eq (#42061) The new name is better anyway, and simplifies life for the blanketSimpArgs linter in #42056: cherry-picked from that PR.

Estimated changes

Modified Mathlib/Order/Partition/Basic.lean

modified theorem Partition.mem_removeBot

modified def Partition.removeBot