Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-04-17 11:13
5f42efa5
View on Github →
feat: port NumberTheory.PellMatiyasevic (
#3083
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/NumberTheory/PellMatiyasevic.lean
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_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_pellZd
added
theorem
Pell.eq_pell_lem
added
theorem
Pell.eq_pow_of_pell
added
theorem
Pell.eq_pow_of_pell_lem
added
theorem
Pell.isPell_iff_mem_unitary
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
theorem
Pell.x_sub_y_dvd_pow_lem
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_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_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