Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-03 18:48 710a76e7

View on Github →

chore(algebra/divisibility): help dot notation on dvd (#8766) Add aliases

  • dvd_mul_of_dvd_left -> has_dvd.dvd.mul_right
  • dvd_mul_of_dvd_right -> has_dvd.dvd.mul_left Add, to help with a few proofs,
  • dvd_rfl
  • dvd_pow_self Use has_dvd.dvd.trans more largely.

Estimated changes

added theorem dvd_rfl
modified theorem one_dvd
modified theorem dvd_lcm_left
modified theorem dvd_lcm_right
modified theorem dvd_pow
added theorem dvd_pow_self
modified theorem pell.asq_pos
modified def pell.az
modified theorem pell.d_pos
modified theorem pell.dvd_of_ysq_dvd
modified theorem pell.dz_val
modified theorem pell.eq_of_xn_modeq'
modified theorem pell.eq_of_xn_modeq
modified theorem pell.eq_of_xn_modeq_le
modified theorem pell.eq_of_xn_modeq_lem1
modified theorem pell.eq_of_xn_modeq_lem2
modified theorem pell.eq_of_xn_modeq_lem3
modified theorem pell.eq_pell
modified theorem pell.eq_pell_lem
modified theorem pell.eq_pell_zd
modified def pell.is_pell
modified theorem pell.is_pell_conj
modified theorem pell.is_pell_mul
modified theorem pell.is_pell_nat
modified theorem pell.is_pell_norm
modified theorem pell.is_pell_one
modified theorem pell.is_pell_pell_zd
modified theorem pell.modeq_of_xn_modeq
modified theorem pell.n_lt_a_pow
modified theorem pell.n_lt_xn
modified def pell.pell
modified theorem pell.pell_eq
modified theorem pell.pell_eqz
modified theorem pell.pell_val
modified def pell.pell_zd
modified theorem pell.pell_zd_add
modified theorem pell.pell_zd_im
modified theorem pell.pell_zd_re
modified theorem pell.pell_zd_sub
modified theorem pell.pell_zd_succ
modified theorem pell.pell_zd_succ_succ
modified theorem pell.x_increasing
modified theorem pell.x_pos
modified theorem pell.x_sub_y_dvd_pow
modified theorem pell.x_sub_y_dvd_pow_lem
modified def pell.xn
modified theorem pell.xn_add
modified theorem pell.xn_ge_a_pow
modified theorem pell.xn_modeq_x2n_add
modified theorem pell.xn_modeq_x2n_add_lem
modified theorem pell.xn_modeq_x2n_sub
modified theorem pell.xn_modeq_x2n_sub_lem
modified theorem pell.xn_modeq_x4n_add
modified theorem pell.xn_modeq_x4n_sub
modified theorem pell.xn_one
modified theorem pell.xn_succ
modified theorem pell.xn_succ_succ
modified theorem pell.xn_zero
modified theorem pell.xy_coprime
modified theorem pell.xy_modeq_yn
modified theorem pell.xy_succ_succ
modified def pell.xz
modified theorem pell.xz_sub
modified theorem pell.xz_succ
modified theorem pell.xz_succ_succ
modified theorem pell.y_dvd_iff
modified theorem pell.y_increasing
modified theorem pell.y_mul_dvd
modified def pell.yn
modified theorem pell.yn_add
modified theorem pell.yn_ge_n
modified theorem pell.yn_modeq_a_sub_one
modified theorem pell.yn_modeq_two
modified theorem pell.yn_one
modified theorem pell.yn_succ
modified theorem pell.yn_succ_succ
modified theorem pell.yn_zero
modified theorem pell.ysq_dvd_yy
modified def pell.yz
modified theorem pell.yz_sub
modified theorem pell.yz_succ
modified theorem pell.yz_succ_succ