Commit 2021-07-02 18:14 dc3a995b

View on Github →

feat(data/nat/gcd.lean): port from Lean 3 (except for pow_dvd_pow_iff) (#20)

  • port data/nat/gcd.lean (except for pow_dvd_pow_iff)
  • minor touchup
  • move Dvd class and notation to top level file, like Mem
  • add copyright header
  • add missing imports
  • gcd_induction -> gcd.induction
  • simplify usages of gcd.induction via the 'induction' tactic
  • remove unused import
  • tiny simplification of gcd_rec proof
  • use eq_zero_of_mul_eq_zero

Estimated changes

added theorem Nat.coprime.gcd_both
added theorem Nat.coprime.gcd_eq_one
added theorem Nat.coprime.gcd_left
added theorem Nat.coprime.gcd_mul
added theorem Nat.coprime.gcd_right
added theorem Nat.coprime.mul
added theorem Nat.coprime.mul_right
added theorem Nat.coprime.pow
added theorem Nat.coprime.pow_left
added theorem Nat.coprime.pow_right
added theorem Nat.coprime.symm
added def Nat.coprime
added theorem Nat.coprime_comm
added theorem Nat.coprime_one_left
added theorem Nat.coprime_one_right
added theorem Nat.coprime_self
added theorem Nat.coprime_zero_left
added theorem Nat.coprime_zero_right
added theorem Nat.dvd_antisymm
added theorem Nat.dvd_gcd
added theorem Nat.dvd_gcd_iff
added theorem Nat.dvd_lcm_left
added theorem Nat.dvd_lcm_right
added theorem Nat.dvd_mod_iff
added theorem Nat.dvd_of_mod_eq_zero
added theorem Nat.dvd_sub
added theorem Nat.eq_one_of_dvd_one
added theorem Nat.exists_coprime'
added theorem Nat.exists_coprime
added theorem Nat.gcd.induction
added theorem Nat.gcd_add_mul_self
added theorem Nat.gcd_assoc
added theorem Nat.gcd_comm
added theorem Nat.gcd_div
added theorem Nat.gcd_dvd
added theorem Nat.gcd_dvd_left
added theorem Nat.gcd_dvd_right
added theorem Nat.gcd_eq_left
added theorem Nat.gcd_eq_right
added theorem Nat.gcd_eq_zero_iff
added theorem Nat.gcd_le_left
added theorem Nat.gcd_le_right
added theorem Nat.gcd_mul_lcm
added theorem Nat.gcd_mul_left
added theorem Nat.gcd_mul_left_left
added theorem Nat.gcd_mul_left_right
added theorem Nat.gcd_mul_right
added theorem Nat.gcd_mul_right_left
added theorem Nat.gcd_one_right
added theorem Nat.gcd_rec
added def Nat.lcm
added theorem Nat.lcm_assoc
added theorem Nat.lcm_comm
added theorem Nat.lcm_dvd
added theorem Nat.lcm_ne_zero
added theorem Nat.lcm_one_left
added theorem Nat.lcm_one_right
added theorem Nat.lcm_self
added theorem Nat.lcm_zero_left
added theorem Nat.lcm_zero_right
added theorem Nat.le_of_dvd
added theorem Nat.mod_eq_zero_of_dvd
added theorem Nat.pos_of_dvd_of_pos