Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-14 01:53 edde6f57

View on Github →

feat(tactic/ring): use ring for rewriting into pretty print format

Estimated changes

Modified tactic/basic.lean

Modified tactic/ring.lean

added theorem tactic.ring.add_neg_eq_sub

added theorem tactic.ring.horner_def'

added theorem tactic.ring.mul_assoc_rev

added inductive tactic.ring.normalize_mode

added theorem tactic.ring.pow_add_rev

added theorem tactic.ring.pow_add_rev_right