Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 12:10 22c42912

View on Github →

chore(number_theory/dioph): Cleanup (#13403) Clean up, including:

  • Move prerequisites to the correct files
  • Make equalities in poly operations defeq
  • Remove defeq abuse around set
  • Slightly golf proofs by tweaking explicitness of lemma arguments Renames

Estimated changes

added theorem list.all₂.imp
added theorem list.all₂_cons
added theorem list.all₂_iff_forall
added theorem list.all₂_map_iff
added def list.all₂
added def option.cons
added theorem option.cons_none_some
modified theorem dioph.abs_poly_dioph
modified theorem dioph.add_dioph
deleted theorem dioph.and_dioph
modified theorem dioph.dioph_comp2
modified theorem dioph.dioph_comp
modified def dioph.dioph_fn
modified theorem dioph.dioph_fn_comp2
modified theorem dioph.dioph_fn_comp
modified theorem dioph.dioph_fn_compn
modified theorem dioph.dioph_fn_vec
modified theorem dioph.dioph_fn_vec_comp1
deleted theorem dioph.dioph_list_all
modified def dioph.dioph_pfun
modified theorem dioph.dioph_pfun_vec
modified theorem dioph.div_dioph
modified theorem dioph.dvd_dioph
modified theorem dioph.eq_dioph
modified theorem dioph.ex1_dioph
modified theorem dioph.ex_dioph
modified theorem dioph.ext
modified theorem dioph.inject_dummies
added theorem dioph.inter
modified theorem dioph.le_dioph
modified theorem dioph.lt_dioph
modified theorem dioph.mod_dioph
modified theorem dioph.modeq_dioph
modified theorem dioph.mul_dioph
modified theorem dioph.ne_dioph
modified theorem dioph.of_no_dummies
deleted theorem dioph.or_dioph
modified theorem dioph.pell_dioph
modified theorem dioph.pow_dioph
modified theorem dioph.proj_dioph
modified theorem dioph.proj_dioph_of_nat
modified theorem dioph.reindex_dioph
modified theorem dioph.reindex_dioph_fn
modified theorem dioph.sub_dioph
added theorem dioph.union
modified theorem dioph.xn_dioph
deleted theorem int.eq_nat_abs_iff_mul
added theorem is_poly.add
added theorem is_poly.neg
modified inductive is_poly
deleted theorem list_all.imp
deleted def list_all
deleted theorem list_all_congr
deleted theorem list_all_cons
deleted theorem list_all_iff_forall
deleted theorem list_all_map
deleted def option.cons
deleted theorem option.cons_head_tail
deleted def poly.add
added theorem poly.add_apply
deleted theorem poly.add_eval
added theorem poly.coe_add
added theorem poly.coe_mul
added theorem poly.coe_neg
added theorem poly.coe_one
added theorem poly.coe_sub
added theorem poly.coe_zero
added theorem poly.const_apply
deleted theorem poly.const_eval
modified theorem poly.ext
deleted theorem poly.isp
added def poly.map
added theorem poly.map_apply
deleted def poly.mul
added theorem poly.mul_apply
deleted theorem poly.mul_eval
deleted def poly.neg
added theorem poly.neg_apply
deleted theorem poly.neg_eval
deleted def poly.one
added theorem poly.one_apply
deleted theorem poly.one_eval
added theorem poly.proj_apply
deleted theorem poly.proj_eval
deleted def poly.remap
deleted theorem poly.remap_eval
deleted def poly.sub
added theorem poly.sub_apply
deleted theorem poly.sub_eval
deleted def poly.subst
deleted theorem poly.subst_eval
modified theorem poly.sumsq_eq_zero
modified theorem poly.sumsq_nonneg
deleted def poly.zero
added theorem poly.zero_apply
deleted theorem poly.zero_eval
deleted def sum.join