Commit 2022-12-22 18:28 4c70fde2

View on Github →

feat: port data.nat.prime (#1156)

depends on #1142

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Prime.lean

added theorem Int.prime_three

added theorem Int.prime_two

added theorem Nat.Prime.coprime_iff_not_dvd

added theorem Nat.Prime.coprime_pow_of_not_dvd

added theorem Nat.Prime.dvd_factorial

added theorem Nat.Prime.dvd_iff_eq

added theorem Nat.Prime.dvd_iff_not_coprime

added theorem Nat.Prime.dvd_mul

added theorem Nat.Prime.dvd_mul_of_dvd_ne

added theorem Nat.Prime.dvd_of_dvd_pow

added theorem Nat.Prime.eq_one_of_pow

added theorem Nat.Prime.eq_one_or_self_of_dvd

added theorem Nat.Prime.eq_two_or_odd'

added theorem Nat.Prime.eq_two_or_odd

added theorem Nat.Prime.even_iff

added theorem Nat.Prime.five_le_of_ne_two_of_ne_three

added theorem Nat.Prime.minFac_eq

added theorem Nat.Prime.mod_two_eq_one_iff_ne_two

added theorem Nat.Prime.mul_eq_prime_sq_iff

added theorem Nat.Prime.ne_one

added theorem Nat.Prime.ne_zero

added theorem Nat.Prime.not_coprime_iff_dvd

added theorem Nat.Prime.not_dvd_mul

added theorem Nat.Prime.not_dvd_one

added theorem Nat.Prime.odd_of_ne_two

added theorem Nat.Prime.one_lt

added theorem Nat.Prime.pos

added theorem Nat.Prime.pow_eq_iff

added theorem Nat.Prime.pow_minFac

added theorem Nat.Prime.pow_not_prime'

added theorem Nat.Prime.pow_not_prime

added theorem Nat.Prime.pred_pos

added theorem Nat.Prime.two_le

added def Nat.Prime

added theorem Nat.Primes.coe_nat_inj

added theorem Nat.Primes.coe_nat_injective

added def Nat.Primes

added theorem Nat.coprime_of_dvd'

added theorem Nat.coprime_of_dvd

added theorem Nat.coprime_of_lt_prime

added theorem Nat.coprime_or_dvd_of_prime

added theorem Nat.coprime_pow_primes

added theorem Nat.coprime_primes

added def Nat.decidablePrime1

added theorem Nat.dvd_of_forall_prime_mul_dvd

added theorem Nat.dvd_prime

added theorem Nat.dvd_prime_pow

added theorem Nat.dvd_prime_two_le

added theorem Nat.eq_one_iff_not_exists_prime_dvd

added theorem Nat.eq_or_coprime_of_le_prime

added theorem Nat.eq_prime_pow_of_dvd_least_prime_pow

added theorem Nat.exists_dvd_of_not_prime2

added theorem Nat.exists_dvd_of_not_prime

added theorem Nat.exists_infinite_primes

added theorem Nat.exists_prime_and_dvd

added theorem Nat.factors_lemma

added theorem Nat.irreducible_iff_nat_prime

added theorem Nat.irreducible_iff_prime

added theorem Nat.le_minFac'

added theorem Nat.le_minFac

added def Nat.minFac

added def Nat.minFacAux

added theorem Nat.minFacAux_has_prop

added theorem Nat.minFac_dvd

added theorem Nat.minFac_eq

added theorem Nat.minFac_eq_one_iff

added theorem Nat.minFac_eq_two_iff

added theorem Nat.minFac_has_prop

added theorem Nat.minFac_le

added theorem Nat.minFac_le_div

added theorem Nat.minFac_le_of_dvd

added theorem Nat.minFac_lemma

added theorem Nat.minFac_one

added theorem Nat.minFac_pos

added theorem Nat.minFac_prime

added theorem Nat.minFac_sq_le_self

added theorem Nat.minFac_zero

added theorem Nat.ne_one_iff_exists_prime_dvd

added theorem Nat.not_bddAbove_setOf_prime

added theorem Nat.not_prime_iff_minFac_lt

added theorem Nat.not_prime_mul'

added theorem Nat.not_prime_mul

added theorem Nat.not_prime_one

added theorem Nat.not_prime_zero

added theorem Nat.pow_minFac

added theorem Nat.prime_def_le_sqrt

added theorem Nat.prime_def_lt''

added theorem Nat.prime_def_lt'

added theorem Nat.prime_def_lt

added theorem Nat.prime_def_minFac

added theorem Nat.prime_dvd_prime_iff_eq

added theorem Nat.prime_iff

added theorem Nat.prime_iff_prime_int

added theorem Nat.prime_mul_iff

added theorem Nat.prime_of_coprime

added theorem Nat.prime_three

added theorem Nat.prime_two

added theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

added theorem Nat.succ_pred_prime