Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-13 03:25 2e2d89ba

View on Github →

feat(tactic/ring): tactic for ring equality

Estimated changes

Modified algebra/group_power.lean

modified theorem add_monoid.smul_one

modified theorem pow_one

Modified data/pnat.lean

modified def nat.to_pnat

Created tactic/basic.lean

Modified tactic/interactive.lean

Modified tactic/norm_num.lean

Created tactic/ring.lean

added def horner

added theorem tactic.ring.const_add_horner

added theorem tactic.ring.horner_add_const

added theorem tactic.ring.horner_add_horner_eq

added theorem tactic.ring.horner_add_horner_gt

added theorem tactic.ring.horner_add_horner_lt

added theorem tactic.ring.horner_atom

added theorem tactic.ring.horner_const_mul

added theorem tactic.ring.horner_horner

added theorem tactic.ring.horner_mul_const

added theorem tactic.ring.horner_mul_horner

added theorem tactic.ring.horner_mul_horner_zero

added theorem tactic.ring.horner_neg

added theorem tactic.ring.horner_pow

added theorem tactic.ring.subst_into_neg

added theorem tactic.ring.subst_into_pow

added theorem tactic.ring.zero_horner