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