Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-15 20:59 25e414d1

View on Github →

feat(tactic/linarith): nlinarith tactic (#2637) Based on Coq's nra tactic, and requested on Zulip.

Estimated changes

Modified src/data/bool.lean

Modified src/data/list/defs.lean

added def list.mmap'_diag

Modified src/tactic/linarith.lean

added theorem linarith.mul_zero_eq

added theorem linarith.zero_mul_eq

Modified test/linarith.lean

deleted theorem test6