Commit 2026-06-30 15:26 b4d8056a

View on Github →

chore(Tactic/Linarith/Parsing): remove local abbrev for TreeMap (#40668) We can now write TreeMap, and Ord.compare is filled in automatically.

Estimated changes

Modified Mathlib/Tactic/Linarith/Parsing.lean

modified def Mathlib.Tactic.Linarith.elimMonom

modified def Mathlib.Tactic.Linarith.toComp

modified def Mathlib.Tactic.Linarith.toCompFold