Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-01 08:02 7191e391

View on Github →

feat(theories/number_theory/dioph): Pell equation, diophantine equations

Estimated changes

added theorem bit0_zero
added theorem bit1_zero
added theorem int.coe_nat_mod
added theorem int.to_nat_coe_nat
added theorem int.to_nat_of_nonneg
modified theorem nat.coprime.gcd_eq_one
modified theorem nat.coprime.symm
added def nat.gcd_a
added def nat.gcd_b
added theorem nat.gcd_eq_gcd_ab
added def nat.xgcd
added def nat.xgcd_aux
added theorem nat.xgcd_aux_P
added theorem nat.xgcd_aux_fst
added theorem nat.xgcd_aux_rec
added theorem nat.xgcd_aux_val
added theorem nat.xgcd_val
added theorem nat.xgcd_zero_left
added theorem nat.modeq.dvd_of_modeq
added theorem nat.modeq.modeq_add
added theorem nat.modeq.modeq_mul
added theorem nat.modeq.modeq_of_dvd
added def nat.modeq
modified def pfun.graph
added theorem pfun.lift_graph
added def arity
added def curry
added theorem dioph.abs_poly_dioph
added theorem dioph.add_dioph
added theorem dioph.and_dioph
added theorem dioph.const_dioph
added theorem dioph.dioph_comp2
added theorem dioph.dioph_comp
added def dioph.dioph_fn
added theorem dioph.dioph_fn_comp1
added theorem dioph.dioph_fn_comp2
added theorem dioph.dioph_fn_comp
added theorem dioph.dioph_fn_compn
added theorem dioph.dioph_fn_vec
added theorem dioph.dioph_list_all
added def dioph.dioph_pfun
added theorem dioph.dioph_pfun_comp1
added theorem dioph.dioph_pfun_vec
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.le_dioph
added theorem dioph.lt_dioph
added theorem dioph.mod_dioph
added theorem dioph.modeq_dioph
added theorem dioph.mul_dioph
added theorem dioph.ne_dioph
added theorem dioph.of_no_dummies
added theorem dioph.or_dioph
added theorem dioph.pell_dioph
added theorem dioph.pow_dioph
added theorem dioph.proj_dioph
added theorem dioph.reindex_dioph
added theorem dioph.reindex_dioph_fn
added theorem dioph.sub_dioph
added theorem dioph.vec_ex1_dioph
added theorem dioph.xn_dioph
added def dioph
added theorem exists_vector_succ
added theorem exists_vector_zero
added def fin2.add
added def fin2.elim0
added def fin2.insert_perm
added def fin2.left
added def fin2.of_nat'
added def fin2.opt_of_nat
added def fin2.remap_left
added inductive fin2
added theorem int.eq_nat_abs_iff_mul
added inductive is_poly
added theorem list_all.imp
added def list_all
added theorem list_all_congr
added theorem list_all_cons
added theorem list_all_iff_forall
added theorem list_all_map
added def option.cons
added def poly.add
added theorem poly.add_eval
added theorem poly.add_val
added def poly.const
added theorem poly.const_eval
added def poly.eval
added def poly.ext
added def poly.induction
added def poly.isp
added def poly.mul
added theorem poly.mul_eval
added theorem poly.mul_val
added def poly.neg
added theorem poly.neg_eval
added theorem poly.neg_val
added def poly.one
added theorem poly.one_eval
added theorem poly.one_val
added def poly.pow
added def poly.proj
added theorem poly.proj_eval
added def poly.remap
added theorem poly.remap_eval
added def poly.sub
added theorem poly.sub_eval
added theorem poly.sub_val
added def poly.subst
added theorem poly.subst_eval
added def poly.sumsq
added theorem poly.sumsq_eq_zero
added theorem poly.sumsq_nonneg
added def poly.zero
added theorem poly.zero_eval
added theorem poly.zero_val
added def poly
added def sum.join
added def uncurry
added inductive vector2
added def vector3.append
added theorem vector3.append_insert
added def vector3.cons
added theorem vector3.cons_elim_cons
added def vector3.cons_fs
added def vector3.cons_fz
added theorem vector3.cons_head_tail
added theorem vector3.eq_nil
added def vector3.head
added def vector3.insert
added theorem vector3.insert_fz
added def vector3.nil
added def vector3.nil_elim
added def vector3.nth
added def vector3.of_fn
added theorem vector3.rec_on_cons
added theorem vector3.rec_on_nil
added def vector3.tail
added def vector3
added def vector_all
added theorem vector_all_iff_forall
added theorem vector_allp.imp
added def vector_allp
added theorem vector_allp_cons
added theorem vector_allp_iff_forall
added theorem vector_allp_nil
added theorem vector_allp_singleton
added def vector_ex
added theorem vector_ex_iff_exists
added theorem pell.asq_pos
added def pell.az
added theorem pell.d_pos
added theorem pell.dvd_of_ysq_dvd
added theorem pell.dz_val
added theorem pell.eq_of_xn_modeq'
added theorem pell.eq_of_xn_modeq
added theorem pell.eq_of_xn_modeq_le
added theorem pell.eq_pell
added theorem pell.eq_pell_lem
added theorem pell.eq_pell_zd
added theorem pell.eq_pow_of_pell
added def pell.is_pell
added def pell.is_pell_mul
added def pell.is_pell_nat
added def pell.is_pell_one
added theorem pell.matiyasevic
added theorem pell.modeq_of_xn_modeq
added def pell.n_lt_a_pow
added theorem pell.n_lt_xn
added def pell.pell
added theorem pell.pell_eq
added theorem pell.pell_eqz
added theorem pell.pell_val
added def pell.pell_zd
added theorem pell.pell_zd_add
added theorem pell.pell_zd_im
added theorem pell.pell_zd_re
added theorem pell.pell_zd_sub
added theorem pell.pell_zd_succ
added theorem pell.pell_zd_succ_succ
added theorem pell.x_increasing
added theorem pell.x_pos
added theorem pell.x_sub_y_dvd_pow
added def pell.xn
added theorem pell.xn_add
added def pell.xn_ge_a_pow
added theorem pell.xn_modeq_x2n_add
added theorem pell.xn_modeq_x2n_sub
added theorem pell.xn_modeq_x4n_add
added theorem pell.xn_modeq_x4n_sub
added theorem pell.xn_one
added theorem pell.xn_succ
added theorem pell.xn_succ_succ
added theorem pell.xn_zero
added theorem pell.xy_coprime
added theorem pell.xy_modeq_of_modeq
added theorem pell.xy_modeq_yn
added theorem pell.xy_succ_succ
added def pell.xz
added theorem pell.xz_sub
added theorem pell.xz_succ
added theorem pell.xz_succ_succ
added theorem pell.y_dvd_iff
added theorem pell.y_increasing
added theorem pell.y_mul_dvd
added def pell.yn
added theorem pell.yn_add
added theorem pell.yn_ge_n
added theorem pell.yn_modeq_two
added theorem pell.yn_one
added theorem pell.yn_succ
added theorem pell.yn_succ_succ
added theorem pell.yn_zero
added theorem pell.ysq_dvd_yy
added def pell.yz
added theorem pell.yz_sub
added theorem pell.yz_succ
added theorem pell.yz_succ_succ
added def zsqrtd.add
added theorem zsqrtd.add_def
added theorem zsqrtd.add_im
added theorem zsqrtd.add_re
added theorem zsqrtd.bit0_im
added theorem zsqrtd.bit0_re
added theorem zsqrtd.bit1_im
added theorem zsqrtd.bit1_re
added theorem zsqrtd.coe_int_im
added theorem zsqrtd.coe_int_re
added theorem zsqrtd.coe_int_val
added theorem zsqrtd.coe_nat_im
added theorem zsqrtd.coe_nat_re
added theorem zsqrtd.coe_nat_val
added def zsqrtd.conj
added theorem zsqrtd.conj_im
added theorem zsqrtd.conj_mul
added theorem zsqrtd.conj_re
added theorem zsqrtd.d_pos
added theorem zsqrtd.decompose
added theorem zsqrtd.ext
added theorem zsqrtd.le_antisymm
added theorem zsqrtd.le_arch
added theorem zsqrtd.le_of_le_le
added theorem zsqrtd.le_refl
added def zsqrtd.mul
added theorem zsqrtd.mul_conj
added theorem zsqrtd.mul_im
added theorem zsqrtd.mul_re
added theorem zsqrtd.muld_val
added def zsqrtd.neg
added theorem zsqrtd.neg_im
added theorem zsqrtd.neg_re
added def zsqrtd.nonneg
added theorem zsqrtd.nonneg_add
added theorem zsqrtd.nonneg_add_lem
added theorem zsqrtd.nonneg_antisymm
added theorem zsqrtd.nonneg_cases
added theorem zsqrtd.nonneg_mul
added theorem zsqrtd.nonneg_mul_lem
added theorem zsqrtd.nonneg_muld
added theorem zsqrtd.nonneg_smul
added def zsqrtd.nonnegg
added theorem zsqrtd.not_sq_le_succ
added def zsqrtd.of_int
added theorem zsqrtd.of_int_eq_coe
added theorem zsqrtd.of_int_im
added theorem zsqrtd.of_int_re
added def zsqrtd.one
added theorem zsqrtd.one_im
added theorem zsqrtd.one_re
added theorem zsqrtd.smul_val
added theorem zsqrtd.smuld_val
added def zsqrtd.sq_le
added theorem zsqrtd.sq_le_add
added theorem zsqrtd.sq_le_add_mixed
added theorem zsqrtd.sq_le_cancel
added theorem zsqrtd.sq_le_mul
added theorem zsqrtd.sq_le_of_le
added theorem zsqrtd.sq_le_smul
added def zsqrtd.sqrtd
added theorem zsqrtd.sqrtd_im
added theorem zsqrtd.sqrtd_re
added def zsqrtd.zero
added theorem zsqrtd.zero_im
added theorem zsqrtd.zero_re
added structure zsqrtd