Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-31 08:43 6a449305

View on Github →

refactor(data/pnat): move data.pnat.prime (#4839) Remove the dependency data.pnat.basic -> data.nat.prime. Needed for #4822.

Estimated changes

deleted theorem nat.primes.coe_pnat_inj
deleted theorem nat.primes.coe_pnat_nat
deleted theorem pnat.coprime.gcd_mul
deleted theorem pnat.coprime.mul
deleted theorem pnat.coprime.mul_right
deleted theorem pnat.coprime.pow
deleted theorem pnat.coprime.symm
deleted def pnat.coprime
deleted theorem pnat.coprime_coe
deleted theorem pnat.coprime_one
deleted theorem pnat.dvd_gcd
deleted theorem pnat.dvd_lcm_left
deleted theorem pnat.dvd_lcm_right
deleted theorem pnat.dvd_prime
deleted theorem pnat.eq_one_of_lt_two
deleted theorem pnat.exists_prime_and_dvd
deleted def pnat.gcd
deleted theorem pnat.gcd_coe
deleted theorem pnat.gcd_comm
deleted theorem pnat.gcd_dvd_left
deleted theorem pnat.gcd_dvd_right
deleted theorem pnat.gcd_eq_left
deleted theorem pnat.gcd_eq_left_iff_dvd
deleted theorem pnat.gcd_eq_right_iff_dvd
deleted theorem pnat.gcd_mul_lcm
deleted theorem pnat.gcd_one
deleted def pnat.lcm
deleted theorem pnat.lcm_coe
deleted theorem pnat.lcm_dvd
deleted theorem pnat.not_prime_one
deleted theorem pnat.one_coprime
deleted theorem pnat.one_gcd
deleted theorem pnat.prime.ne_one
deleted theorem pnat.prime.not_dvd_one
deleted theorem pnat.prime.one_lt
deleted def pnat.prime
deleted theorem pnat.prime_two
added theorem pnat.coprime.gcd_mul
added theorem pnat.coprime.mul
added theorem pnat.coprime.mul_right
added theorem pnat.coprime.pow
added theorem pnat.coprime.symm
added def pnat.coprime
added theorem pnat.coprime_coe
added theorem pnat.coprime_one
added theorem pnat.dvd_gcd
added theorem pnat.dvd_lcm_left
added theorem pnat.dvd_lcm_right
added theorem pnat.dvd_prime
added theorem pnat.eq_one_of_lt_two
added def pnat.gcd
added theorem pnat.gcd_coe
added theorem pnat.gcd_comm
added theorem pnat.gcd_dvd_left
added theorem pnat.gcd_dvd_right
added theorem pnat.gcd_eq_left
added theorem pnat.gcd_mul_lcm
added theorem pnat.gcd_one
added def pnat.lcm
added theorem pnat.lcm_coe
added theorem pnat.lcm_dvd
added theorem pnat.not_prime_one
added theorem pnat.one_coprime
added theorem pnat.one_gcd
added theorem pnat.prime.ne_one
added theorem pnat.prime.not_dvd_one
added theorem pnat.prime.one_lt
added def pnat.prime
added theorem pnat.prime_two