Commit 2023-04-17 11:13 5f42efa5

View on Github →

feat: port NumberTheory.PellMatiyasevic (#3083)

Estimated changes

added def Pell.IsPell
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_pellZd
added theorem Pell.eq_pell_lem
added theorem Pell.eq_pow_of_pell
added theorem Pell.isPell_mul
added theorem Pell.isPell_nat
added theorem Pell.isPell_norm
added theorem Pell.isPell_one
added theorem Pell.isPell_pellZd
added theorem Pell.isPell_star
added theorem Pell.matiyasevic
added theorem Pell.modEq_of_xn_modEq
added theorem Pell.n_lt_a_pow
added theorem Pell.n_lt_xn
added def Pell.pell
added def Pell.pellZd
added theorem Pell.pellZd_add
added theorem Pell.pellZd_im
added theorem Pell.pellZd_re
added theorem Pell.pellZd_sub
added theorem Pell.pellZd_succ
added theorem Pell.pellZd_succ_succ
added theorem Pell.pell_eq
added theorem Pell.pell_eqz
added theorem Pell.pell_val
added theorem Pell.strictMono_x
added theorem Pell.strictMono_y
added theorem Pell.x_pos
added theorem Pell.x_sub_y_dvd_pow
added def Pell.xn
added theorem Pell.xn_add
added theorem 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_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