OAI/NumberTheory/Jacobsthal/Primes/SmallEffectivePrimeSplit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosVarianceEffective.full_cofactor_coprime_small line 13
2. theorem OAI.Erdos970.ErdosVarianceEffective.small_dvd_effectiveModulus_iff line 22
3. theorem OAI.Erdos970.ErdosVarianceEffective.small_effective_avoidance line 34