New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - fix(NumberTheory/FermatPsp): Update definition and theorem names #6371
Conversation
(Just a reminder that on the mathlib4 repo, if authors don't self-label with |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Modulo the rw [mul_comm]
issue which I flag, this looks fine to me.
This helps remove two "rw" statements
Thanks! maintainer merge |
🚀 Pull request has been placed on the maintainer queue by kbuzzard. |
Thanks! bors merge |
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.
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
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.
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.
Fix some definition and theorem names in NumberTheory/FermatPsp. Most of these definitions were previously under the
FermatPsp
namespace. This PR removes theFermatPsp
namespace and places all the definitions under theNat
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 theMathlib.Data.Nat.Prime
import because it is transitively included in theMathlib.FieldTheory.Finite.Basic
import.I made the
FermatPsp
file when I was newer to Lean, and I think the new names are a bit closer to the rest of the naming convention in Mathlib. I am still new to the Lean 4 naming conventions so please let me know if I made any mistakes.In the future, I might make the definition of
Nat.ProbablePrime
rely on modular arithmetic rather than divisibility.