Commit 2025-04-30 13:43 fafe8409

View on Github →

chore: use Std.TreeMap in linarith (#24367) This PR avoids use of Batteries.RBMap in the implementation of linarith, where the new Std.TreeMap suffices.

Estimated changes

Modified Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean

added def Std.TreeSet.sdiff

added def Std.TreeSet.union

Modified Mathlib/Tactic/Linarith/Parsing.lean

modified def Linarith.Monom.one

modified def Linarith.Sum.one

modified def Linarith.one

added def Std.TreeMap.beq