Commit 2024-07-02 02:30 12473136

View on Github →

chore(Data/Nat): split Prime.lean (#14286) Splitting Prime.lean into Defs, Basic. The split aims at separation of defs and needed lemmas from everything else. With this split 13/18 Mathlib modules no longer import the whole Prime.lean. Prime/Defs.lean is about half the size. Motivation is a circular dependency that would prevent me from adding a lemma to Prime.lean. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/split.20Nat.2FPrime.2Elean

Estimated changes

Modified Archive/Imo/Imo1959Q1.lean

Modified Archive/Imo/Imo1988Q6.lean

Modified Archive/Imo/Imo2008Q3.lean

Modified Archive/Imo/Imo2019Q4.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/CharP/Defs.lean

Modified Mathlib/Algebra/CharP/ExpChar.lean

Modified Mathlib/Algebra/Order/Floor/Prime.lean

Modified Mathlib/Combinatorics/Schnirelmann.lean

Modified Mathlib/Data/Int/NatPrime.lean

Modified Mathlib/Data/Nat/Choose/Dvd.lean

Modified Mathlib/Data/Nat/Factors.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

Created Mathlib/Data/Nat/Prime/Basic.lean

added theorem Int.prime_three

added theorem Int.prime_two

added theorem Nat.Prime.coprime_pow_of_not_dvd

added theorem Nat.Prime.dvd_factorial

added theorem Nat.Prime.dvd_iff_not_coprime

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_two_or_odd'

added theorem Nat.Prime.eq_two_or_odd

added theorem Nat.Prime.even_iff

added theorem Nat.Prime.even_sub_one

added theorem Nat.Prime.five_le_of_ne_two_of_ne_three

added theorem Nat.Prime.mod_two_eq_one_iff_ne_two

added theorem Nat.Prime.mul_eq_prime_sq_iff

added theorem Nat.Prime.not_coprime_iff_dvd

added theorem Nat.Prime.not_dvd_mul

added theorem Nat.Prime.not_prime_pow'

added theorem Nat.Prime.not_prime_pow

added theorem Nat.Prime.odd_of_ne_two

added theorem Nat.Prime.pow_eq_iff

added theorem Nat.Prime.pow_inj

added theorem Nat.Prime.pow_minFac

added theorem Nat.Prime.pred_pos

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 theorem Nat.coprime_two_left

added theorem Nat.coprime_two_right

added theorem Nat.dvd_of_forall_prime_mul_dvd

added theorem Nat.dvd_prime_pow

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_mul_pow_lt_factorial

added theorem Nat.exists_pow_lt_factorial

added theorem Nat.exists_prime_mul_pow_lt_factorial

added theorem Nat.factors_lemma

added theorem Nat.irreducible_iff_prime

added theorem Nat.ne_one_iff_exists_prime_dvd

added theorem Nat.not_bddAbove_setOf_prime

added theorem Nat.not_prime_iff_exists_dvd_lt

added theorem Nat.not_prime_iff_exists_dvd_ne

added theorem Nat.not_prime_of_dvd_of_lt

added theorem Nat.not_prime_of_dvd_of_ne

added theorem Nat.pow_minFac

added theorem Nat.prime_iff_prime_int

added theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

added theorem Nat.succ_pred_prime

Renamed Mathlib/Data/Nat/Prime.lean to Mathlib/Data/Nat/Prime/Defs.lean

deleted theorem Int.prime_three

deleted theorem Int.prime_two

deleted theorem Nat.Prime.coprime_pow_of_not_dvd

deleted theorem Nat.Prime.dvd_factorial

deleted theorem Nat.Prime.dvd_iff_not_coprime

deleted theorem Nat.Prime.dvd_mul_of_dvd_ne

deleted theorem Nat.Prime.dvd_of_dvd_pow

deleted theorem Nat.Prime.eq_one_of_pow

deleted theorem Nat.Prime.eq_two_or_odd'

deleted theorem Nat.Prime.eq_two_or_odd

deleted theorem Nat.Prime.even_iff

deleted theorem Nat.Prime.even_sub_one

deleted theorem Nat.Prime.five_le_of_ne_two_of_ne_three

deleted theorem Nat.Prime.mod_two_eq_one_iff_ne_two

deleted theorem Nat.Prime.mul_eq_prime_sq_iff

deleted theorem Nat.Prime.not_coprime_iff_dvd

deleted theorem Nat.Prime.not_dvd_mul

deleted theorem Nat.Prime.not_prime_pow'

deleted theorem Nat.Prime.not_prime_pow

deleted theorem Nat.Prime.odd_of_ne_two

deleted theorem Nat.Prime.pow_eq_iff

deleted theorem Nat.Prime.pow_inj

deleted theorem Nat.Prime.pow_minFac

deleted theorem Nat.Prime.pred_pos

deleted theorem Nat.coprime_of_dvd'

deleted theorem Nat.coprime_of_lt_prime

deleted theorem Nat.coprime_or_dvd_of_prime

deleted theorem Nat.coprime_pow_primes

deleted theorem Nat.coprime_primes

deleted theorem Nat.coprime_two_left

deleted theorem Nat.coprime_two_right

deleted theorem Nat.dvd_of_forall_prime_mul_dvd

deleted theorem Nat.dvd_prime_pow

deleted theorem Nat.eq_one_iff_not_exists_prime_dvd

deleted theorem Nat.eq_or_coprime_of_le_prime

deleted theorem Nat.eq_prime_pow_of_dvd_least_prime_pow

deleted theorem Nat.exists_dvd_of_not_prime2

deleted theorem Nat.exists_dvd_of_not_prime

deleted theorem Nat.exists_infinite_primes

deleted theorem Nat.exists_mul_pow_lt_factorial

deleted theorem Nat.exists_pow_lt_factorial

deleted theorem Nat.exists_prime_mul_pow_lt_factorial

deleted theorem Nat.factors_lemma

deleted theorem Nat.irreducible_iff_prime

deleted theorem Nat.ne_one_iff_exists_prime_dvd

deleted theorem Nat.not_bddAbove_setOf_prime

deleted theorem Nat.not_prime_iff_exists_dvd_lt

deleted theorem Nat.not_prime_iff_exists_dvd_ne

deleted theorem Nat.not_prime_of_dvd_of_lt

deleted theorem Nat.not_prime_of_dvd_of_ne

deleted theorem Nat.pow_minFac

deleted theorem Nat.prime_iff_prime_int

deleted theorem Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

deleted theorem Nat.succ_pred_prime

Modified Mathlib/Data/Nat/PrimeNormNum.lean

Modified Mathlib/Data/Num/Prime.lean

Modified Mathlib/Data/PNat/Prime.lean

Modified Mathlib/Dynamics/PeriodicPts.lean

Modified Mathlib/FieldTheory/Tower.lean

Modified Mathlib/Logic/Godel/GodelBetaFunction.lean

Modified Mathlib/ModelTheory/Algebra/Field/CharP.lean

Modified Mathlib/NumberTheory/Primorial.lean

Modified Mathlib/Tactic/NormNum/Prime.lean

Modified test/LibrarySearch/basic.lean

Modified test/hint.lean

Modified test/observe.lean

Modified test/rewrites.lean

Modified test/slim_check.lean