Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-12 22:37 0865bce5

View on Github →

fix(tactic/ring): fix normalization bugs fixes #84

Estimated changes

Modified tactic/ring.lean

modified theorem tactic.ring.horner_add_horner_gt

modified theorem tactic.ring.horner_add_horner_lt