Commit 2023-06-11 15:31 fe6b4e5d

View on Github →

feat: port NumberTheory.Dioph (#4914)

Estimated changes

added def Dioph.DiophFn
added theorem Dioph.DiophList.all₂
added def Dioph.DiophPfun
added theorem Dioph.abs_poly_dioph
added theorem Dioph.add_dioph
added theorem Dioph.const_dioph
added theorem Dioph.diophFn_comp1
added theorem Dioph.diophFn_comp2
added theorem Dioph.diophFn_comp
added theorem Dioph.diophFn_compn
added theorem Dioph.diophFn_iff_pFun
added theorem Dioph.diophFn_vec
added theorem Dioph.diophPfun_comp1
added theorem Dioph.diophPfun_vec
added theorem Dioph.dioph_comp2
added theorem Dioph.dioph_comp
added theorem Dioph.div_dioph
added theorem Dioph.dom_dioph
added theorem Dioph.dvd_dioph
added theorem Dioph.eq_dioph
added theorem Dioph.ex1_dioph
added theorem Dioph.ex_dioph
added theorem Dioph.ext
added theorem Dioph.inject_dummies
added theorem Dioph.inter
added theorem Dioph.le_dioph
added theorem Dioph.lt_dioph
added theorem Dioph.modEq_dioph
added theorem Dioph.mod_dioph
added theorem Dioph.mul_dioph
added theorem Dioph.ne_dioph
added theorem Dioph.of_no_dummies
added theorem Dioph.pell_dioph
added theorem Dioph.pow_dioph
added theorem Dioph.proj_dioph
added theorem Dioph.reindex_dioph
added theorem Dioph.reindex_diophFn
added theorem Dioph.sub_dioph
added theorem Dioph.union
added theorem Dioph.vec_ex1_dioph
added theorem Dioph.xn_dioph
added def Dioph
added theorem IsPoly.add
added theorem IsPoly.neg
added inductive IsPoly
added theorem Poly.add_apply
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 def Poly.const
added theorem Poly.const_apply
added theorem Poly.ext
added theorem Poly.induction
added def Poly.map
added theorem Poly.map_apply
added theorem Poly.mul_apply
added theorem Poly.neg_apply
added theorem Poly.one_apply
added def Poly.proj
added theorem Poly.proj_apply
added theorem Poly.sub_apply
added def Poly.sumsq
added theorem Poly.sumsq_eq_zero
added theorem Poly.sumsq_nonneg
added theorem Poly.zero_apply
added def Poly