Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-04 21:23 b1981c94

View on Github →

chore(theories/number_theory/dioph): cleanup

Estimated changes

modified theorem dioph.abs_poly_dioph
modified theorem dioph.of_no_dummies
modified theorem poly.add_eval
deleted theorem poly.add_val
modified theorem poly.const_eval
deleted def poly.eval
modified def poly.ext
modified def poly.isp
modified theorem poly.mul_eval
deleted theorem poly.mul_val
modified theorem poly.neg_eval
deleted theorem poly.neg_val
modified theorem poly.one_eval
deleted theorem poly.one_val
modified theorem poly.proj_eval
modified theorem poly.remap_eval
modified theorem poly.sub_eval
deleted theorem poly.sub_val
modified def poly.subst
modified theorem poly.subst_eval
modified theorem poly.sumsq_eq_zero
modified theorem poly.sumsq_nonneg
modified theorem poly.zero_eval
deleted theorem poly.zero_val
deleted inductive vector2