Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-25 05:29 516b254d

View on Github →

feat(tactic/ring2): alternative ring tactic

Estimated changes

Modified data/num/lemmas.lean

modified theorem num.cast_sub'

added theorem num.to_znum_inj

added theorem znum.abs_to_znum

Created tactic/ring2.lean

added theorem tactic.ring2.correctness

added def tactic.ring2.csring_expr.eval

added inductive tactic.ring2.csring_expr

added def tactic.ring2.horner_expr.add

added def tactic.ring2.horner_expr.add_aux

added def tactic.ring2.horner_expr.add_const

added def tactic.ring2.horner_expr.atom

added def tactic.ring2.horner_expr.cseval

added theorem tactic.ring2.horner_expr.cseval_add

added theorem tactic.ring2.horner_expr.cseval_add_const

added theorem tactic.ring2.horner_expr.cseval_atom

added theorem tactic.ring2.horner_expr.cseval_horner'

added theorem tactic.ring2.horner_expr.cseval_mul

added theorem tactic.ring2.horner_expr.cseval_mul_const

added theorem tactic.ring2.horner_expr.cseval_of_csexpr

added theorem tactic.ring2.horner_expr.cseval_pow

added def tactic.ring2.horner_expr.horner'

added def tactic.ring2.horner_expr.inv

added def tactic.ring2.horner_expr.is_cs

added def tactic.ring2.horner_expr.mul

added def tactic.ring2.horner_expr.mul_aux

added def tactic.ring2.horner_expr.mul_const

added def tactic.ring2.horner_expr.neg

added def tactic.ring2.horner_expr.of_csexpr

added def tactic.ring2.horner_expr.pow

added def tactic.ring2.horner_expr.repr

added inductive tactic.ring2.horner_expr

added def tactic.ring2.tree.get

added def tactic.ring2.tree.index_of

added def tactic.ring2.tree.of_rbnode

added inductive tactic.ring2.{u}