Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-26 18:11 a66d07e2

View on Github →

chore(number_theory/pell*): rename files, update doc (#18503) Following a suggestion by @ocfnash in a comment to [#18484](https://github.com/leanprover-community/mathlib/pull/18484), this

  • renames number_theory.pell to number_theory.pell_matiyasevic
  • renames number_theory.pell_general to number_theory.pell
  • updates documentation accordingly
  • moves the "TODO" note from pell_matiyasevic to pell (and updates it) See also this Zulip thread.

Estimated changes

deleted theorem pell.asq_pos
deleted def pell.az
deleted theorem pell.d_pos
deleted theorem pell.dvd_of_ysq_dvd
deleted theorem pell.dz_val
deleted theorem pell.eq_of_xn_modeq'
deleted theorem pell.eq_of_xn_modeq
deleted theorem pell.eq_of_xn_modeq_le
deleted theorem pell.eq_of_xn_modeq_lem1
deleted theorem pell.eq_of_xn_modeq_lem2
deleted theorem pell.eq_of_xn_modeq_lem3
deleted theorem pell.eq_pell
deleted theorem pell.eq_pell_lem
deleted theorem pell.eq_pell_zd
deleted theorem pell.eq_pow_of_pell
deleted theorem pell.eq_pow_of_pell_lem
deleted def pell.is_pell
deleted theorem pell.is_pell_conj
deleted theorem pell.is_pell_mul
deleted theorem pell.is_pell_nat
deleted theorem pell.is_pell_norm
deleted theorem pell.is_pell_one
deleted theorem pell.is_pell_pell_zd
deleted theorem pell.matiyasevic
deleted theorem pell.modeq_of_xn_modeq
deleted theorem pell.n_lt_a_pow
deleted theorem pell.n_lt_xn
deleted def pell.pell
deleted theorem pell.pell_eq
deleted theorem pell.pell_eqz
deleted theorem pell.pell_val
deleted def pell.pell_zd
deleted theorem pell.pell_zd_add
deleted theorem pell.pell_zd_im
deleted theorem pell.pell_zd_re
deleted theorem pell.pell_zd_sub
deleted theorem pell.pell_zd_succ
deleted theorem pell.pell_zd_succ_succ
deleted theorem pell.strict_mono_x
deleted theorem pell.strict_mono_y
deleted theorem pell.x_pos
deleted theorem pell.x_sub_y_dvd_pow
deleted theorem pell.x_sub_y_dvd_pow_lem
deleted def pell.xn
deleted theorem pell.xn_add
deleted theorem pell.xn_ge_a_pow
deleted theorem pell.xn_modeq_x2n_add
deleted theorem pell.xn_modeq_x2n_add_lem
deleted theorem pell.xn_modeq_x2n_sub
deleted theorem pell.xn_modeq_x2n_sub_lem
deleted theorem pell.xn_modeq_x4n_add
deleted theorem pell.xn_modeq_x4n_sub
deleted theorem pell.xn_one
deleted theorem pell.xn_succ
deleted theorem pell.xn_succ_succ
deleted theorem pell.xn_zero
deleted theorem pell.xy_coprime
deleted theorem pell.xy_modeq_of_modeq
deleted theorem pell.xy_modeq_yn
deleted theorem pell.xy_succ_succ
deleted def pell.xz
deleted theorem pell.xz_sub
deleted theorem pell.xz_succ
deleted theorem pell.xz_succ_succ
deleted theorem pell.y_dvd_iff
deleted theorem pell.y_mul_dvd
deleted def pell.yn
deleted theorem pell.yn_add
deleted theorem pell.yn_ge_n
deleted theorem pell.yn_modeq_a_sub_one
deleted theorem pell.yn_modeq_two
deleted theorem pell.yn_one
deleted theorem pell.yn_succ
deleted theorem pell.yn_succ_succ
deleted theorem pell.yn_zero
deleted theorem pell.ysq_dvd_yy
deleted def pell.yz
deleted theorem pell.yz_sub
deleted theorem pell.yz_succ
deleted theorem pell.yz_succ_succ
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 theorem pell.is_pell_conj
added theorem pell.is_pell_mul
added theorem pell.is_pell_nat
added theorem pell.is_pell_norm
added theorem pell.is_pell_one
added theorem pell.is_pell_pell_zd
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 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.strict_mono_x
added theorem pell.strict_mono_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