Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-03 12:46
1ca67409
View on Github →
feat: port NumberTheory.FermatPsp (
#4605
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/NumberTheory/FermatPsp.lean
added
def
FermatPsp.ProbablePrime
added
theorem
FermatPsp.base_one
added
theorem
FermatPsp.coprime_of_fermatPsp
added
theorem
FermatPsp.coprime_of_probablePrime
added
theorem
FermatPsp.exists_infinite_pseudoprimes
added
theorem
FermatPsp.frequently_atTop_fermatPsp
added
theorem
FermatPsp.infinite_setOf_prime_modeq_one
added
theorem
FermatPsp.probablePrime_iff_modEq
added
def
FermatPsp