OAI/NumberTheory/Jacobsthal/Primes/PrimeHitRepresentative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosInverseHits.modEq_prime_product_iff line 11
2. theorem OAI.Erdos970.ErdosInverseHits.exists_prime_hit_representative line 28
3. def OAI.Erdos970.ErdosInverseHits.primeHitRepresentative line 65
4. theorem OAI.Erdos970.ErdosInverseHits.primeHitRepresentative_spec line 68