Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-14 15:09 85b8bdcb

View on Github →

perf(tactic/linarith): use key/value lists instead of rb_maps to represent linear expressions (#3004) This has essentially no effect on the test file, but scales much better. See discussion at https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for.20teaching/topic/Real.20analysis for an example which is in reach with this change.

Estimated changes