Commit 2023-07-20 01:29 11832fad

View on Github →

feat: removeNe preprocessor for splitting on inequalities in linarith (#6014)

Estimated changes

Modified Mathlib/Tactic/Linarith/Datatypes.lean

Modified Mathlib/Tactic/Linarith/Frontend.lean

Modified Mathlib/Tactic/Linarith/Preprocessing.lean

added def Linarith.removeNe

Modified test/linarith.lean