Documentation Verification Report

FermatPsp

📁 Source: Mathlib/NumberTheory/FermatPsp.lean

Statistics

Metric	Count
Definitions `FermatPsp`, `ProbablePrime`, `decidableProbablePrime`, `decidablePsp`	4
Theorems `coprime_of_fermatPsp`, `coprime_of_probablePrime`, `exists_infinite_pseudoprimes`, `fermatPsp_base_one`, `frequently_atTop_fermatPsp`, `infinite_setOf_pseudoprimes`, `probablePrime_iff_modEq`	7
Total	11

Nat

Definitions

Name	Category	Theorems
`FermatPsp` 📖	MathDef	4 math math: `frequently_atTop_fermatPsp`, `fermatPsp_base_one`, `infinite_setOf_pseudoprimes`, `exists_infinite_pseudoprimes`
`ProbablePrime` 📖	MathDef	1 math math: `probablePrime_iff_modEq`
`decidableProbablePrime` 📖	CompOp	—
`decidablePsp` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_of_fermatPsp` 📖	—	`FermatPsp`	—	—	`coprime_of_probablePrime`
`coprime_of_probablePrime` 📖	—	`ProbablePrime`	—	—	`coprime_of_dvd` `Prime.not_dvd_one` `dvd_of_mul_right_dvd` `dvd_pow_self`
`exists_infinite_pseudoprimes` 📖	mathematical	—	`FermatPsp`	—	`exists_infinite_primes` `pos_of_gt` `instCanonicallyOrderedAdd` `pow_le_pow_left'` `instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `tsub_pos_of_lt` `instOrderedSub` `lt_of_lt_of_le` `instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `instCharZero` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `le_trans` `lt_of_le_of_lt` `le_of_lt` `not_prime_mul` `fermatPsp_base_one`
`fermatPsp_base_one` 📖	mathematical	`Prime`	`FermatPsp`	—	`dvd_zero` `one_pow` `tsub_self` `instCanonicallyOrderedAdd` `instOrderedSub`
`frequently_atTop_fermatPsp` 📖	mathematical	—	`Filter.Frequently` `FermatPsp` `Filter.atTop` `instPreorder`	—	`Filter.frequently_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `instArchimedeanNat` `exists_infinite_pseudoprimes`
`infinite_setOf_pseudoprimes` 📖	mathematical	—	`Set.Infinite` `setOf` `FermatPsp`	—	`frequently_atTop_iff_infinite` `frequently_atTop_fermatPsp`
`probablePrime_iff_modEq` 📖	mathematical	—	`ProbablePrime` `ModEq` `Monoid.toNatPow` `instMonoid`	—	`one_le_pow₀` `instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `ModEq.comm` `modEq_of_dvd` `ModEq.dvd`

---

← Back to Index