Commit 2023-08-10 10:11 21202466

fix(NumberTheory/FermatPsp): Update definition and theorem names (#6371) Fix some definition and theorem names in NumberTheory/FermatPsp. Most of these definitions were previously under the FermatPsp namespace. This PR removes the FermatPsp namespace and places all the definitions under the Nat namespace. The following are the main changes made to names:

• FermatPsp.ProbablePrime -> Nat.ProbablePrime
• FermatPsp -> Nat.FermatPsp
• FermatPsp.coprime_of_probablePrime -> Nat.coprime_of_probablePrime
• FermatPsp.probablePrime_iff_modEq -> Nat.probablePrime_iff_modEq
• FermatPsp.coprime_of_fermatPsp -> Nat.coprime_of_fermatPsp
• FermatPsp.base_one -> Nat.fermatPsp_base_one
• FermatPsp.exists_infinite_pseudoprimes -> Nat.exists_infinite_pseudoprimes
• FermatPsp.frequently_atTop_fermatPsp -> Nat.frequently_atTop_fermatPsp
• FermatPsp.infinite_setOf_prime_modeq_one -> Nat.infinite_setOf_pseudoprimes The last name was originally a mistake that came from the proof I used as reference. This PR additionally contains a few fixes for the proofs that were needed because they are now in the Nat namespace. It also removes the Mathlib.Data.Nat.Prime import because it is transitively included in the Mathlib.FieldTheory.Finite.Basic import.