[Merged by Bors] - chore(Data/Nat): split Prime.lean

[rwst]

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

---

[github-actions]

PR summary 7e4b3ac8c3

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.PNat.Prime	412	400	-12 (-2.91%)
Mathlib.Tactic.NormNum.Prime	420	411	-9 (-2.14%)
Mathlib.Algebra.CharP.Defs	455	454	-1 (-0.22%)

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[rwst]

The following files now import the shorter Prime/Defs:

Mathlib/Tactic/NormNum/Prime.lean
Mathlib/NumberTheory/Primorial.lean
Mathlib/FieldTheory/Tower.lean
Mathlib/Combinatorics/Schnirelmann.lean
Mathlib/Logic/Godel/GodelBetaFunction.lean
Mathlib/Algebra/CharP/Defs.lean
Mathlib/Algebra/CharP/ExpChar.lean
Mathlib/ModelTheory/Algebra/Field/CharP.lean
Mathlib/Data/Nat/Multiplicity.lean
Mathlib/Data/Nat/Prime/Basic.lean
Mathlib/Data/Nat/PrimeNormNum.lean
Mathlib/Data/Num/Prime.lean
Mathlib/Data/PNat/Prime.lean
Archive/Imo/Imo2008Q3.lean
Archive/Imo/Imo1988Q6.lean
test/slim_check.lean
test/hint.lean
test/rewrites.lean
test/LibrarySearch/basic.lean

The follwing files still import the full Prime/Basic (dependency given):

Mathlib/Dynamics/PeriodicPts.lean
  l.424: eq_prime_pow_of_dvd_least_prime_pow
Mathlib/Algebra/Order/Floor/Prime.lean
  l.24: exists_prime_mul_pow_lt_factorial
Mathlib/Data/Nat/Choose/Dvd.lean
  l.26,28: dvd_factorial
Mathlib/Data/Nat/Factors.lean
  l.41,62,77,101: factors_lemma
  l.325: eq_two_or_odd
Mathlib/Data/Int/NatPrime.lean
  l.31: succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul
Archive/Imo/Imo1959Q1.lean
  l.37: coprime_of_dvd'
Archive/Imo/Imo2019Q4.lean (import was added because Multiplicity no longer imports full Prime.lean)
  l.45: prime_two
test/observe.lean
  ?

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 7e4b3ac.
There were significant changes against commit 03cf112:

  Benchmark   Metric    Change
  ============================
- build       linting     5.0%

[kim-em]

@mattrobball, this is just noise, right??

If so, I'm happy to proceed.

[mattrobball]

Yes, we should crank up the limits for this on the benchmarking server

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style