Commit 2022-12-02 17:14 69dcf627

View on Github →

feat: nlinarith (#819)

Estimated changes

Modified Mathlib/Lean/Expr/Traverse.lean

added def Lean.Expr.foldlM

Modified Mathlib/Tactic/Linarith/Frontend.lean

Modified Mathlib/Tactic/Linarith/Lemmas.lean

added theorem Linarith.mul_zero_eq

added theorem Linarith.zero_mul_eq

added theorem mul_nonneg_of_nonpos_of_nonpos

added theorem mul_pos_of_neg_of_neg

added theorem mul_self_nonneg

added theorem sq_nonneg

Modified Mathlib/Tactic/Linarith/Preprocessing.lean

added def Linarith.defaultPreprocessors

deleted def Linarith.default_preprocessors

added def Linarith.nlinarithExtras

Modified test/linarith.lean

added theorem bar

added theorem norm_eq_zero_iff

added theorem norm_nonpos_left

added theorem norm_nonpos_right

added theorem norm_zero_left