Mathlib Changelog
Changelog
About
Github
Commit
2017-12-01 08:02
7191e391
View on Github →
feat(theories/number_theory/dioph): Pell equation, diophantine equations
Estimated changes
Modified
algebra/group.lean
added
theorem
bit0_zero
added
theorem
bit1_zero
Modified
data/int/basic.lean
added
theorem
int.coe_nat_mod
added
theorem
int.mod_add_cancel_left
added
theorem
int.mod_add_cancel_right
added
theorem
int.mod_eq_mod_iff_mod_sub_eq_zero
deleted
theorem
int.mod_eq_mod_of_add_mod_eq_add_mod_left
deleted
theorem
int.mod_eq_mod_of_add_mod_eq_add_mod_right
added
theorem
int.mod_sub_cancel_right
added
theorem
int.to_nat_coe_nat
added
theorem
int.to_nat_of_nonneg
Modified
data/nat/gcd.lean
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
Created
data/nat/modeq.lean
added
theorem
nat.modeq.chinese_remainder
added
theorem
nat.modeq.dvd_of_modeq
added
theorem
nat.modeq.modeq_add
added
theorem
nat.modeq.modeq_add_cancel_left
added
theorem
nat.modeq.modeq_add_cancel_right
added
theorem
nat.modeq.modeq_iff_dvd
added
theorem
nat.modeq.modeq_mul
added
theorem
nat.modeq.modeq_mul_left'
added
theorem
nat.modeq.modeq_mul_left
added
theorem
nat.modeq.modeq_mul_right'
added
theorem
nat.modeq.modeq_mul_right
added
theorem
nat.modeq.modeq_of_dvd
added
theorem
nat.modeq.modeq_of_dvd_of_modeq
added
theorem
nat.modeq.modeq_zero_iff
added
def
nat.modeq
Modified
data/pfun.lean
modified
def
pfun.graph
added
theorem
pfun.lift_graph
Created
theories/number_theory/dioph.lean
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_iff_pfun
added
theorem
dioph.dioph_fn_vec
added
theorem
dioph.dioph_fn_vec_comp1
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.inject_dummies_lem
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
def
dioph.proj_dioph_of_nat
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
option.cons_head_tail
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
def
vector3.append_add
added
def
vector3.append_cons
added
theorem
vector3.append_insert
added
def
vector3.append_left
added
def
vector3.append_nil
added
def
vector3.cons
added
def
vector3.cons_elim
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
def
vector3.insert_fs
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
Created
theories/number_theory/pell.lean
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_of_xn_modeq_lem1
added
theorem
pell.eq_of_xn_modeq_lem2
added
theorem
pell.eq_of_xn_modeq_lem3
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
theorem
pell.eq_pow_of_pell_lem
added
def
pell.is_pell
added
def
pell.is_pell_conj
added
def
pell.is_pell_mul
added
def
pell.is_pell_nat
added
def
pell.is_pell_norm
added
def
pell.is_pell_one
added
def
pell.is_pell_pell_zd
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
theorem
pell.x_sub_y_dvd_pow_lem
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_add_lem
added
theorem
pell.xn_modeq_x2n_sub
added
theorem
pell.xn_modeq_x2n_sub_lem
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_a_sub_one
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.divides_sq_eq_zero
added
theorem
zsqrtd.divides_sq_eq_zero_z
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_iff_zero_le
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
def
zsqrtd.nonnegg_cases_left
added
def
zsqrtd.nonnegg_cases_right
added
def
zsqrtd.nonnegg_comm
added
def
zsqrtd.nonnegg_neg_pos
added
def
zsqrtd.nonnegg_pos_neg
added
theorem
zsqrtd.not_divides_square
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