Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linarith.mul_nonpos

Modification history

2020-08-15 20:42

src/tactic/linarith/lemmas.lean

fix(*): remove usages of ge/gt (#3808) …

Modified linarith.mul_nonpos View on Github →

2020-06-24 10:22

src/tactic/linarith.lean

refactor(tactic/linarith): big refactor and docs (#3113) …

Modified linarith.mul_nonpos View on Github →

2018-09-02 20:07

tactic/linarith.lean

feat(tactic): add linear arithmetic tactic (#301) …

Added linarith.mul_nonpos View on Github →