OAI/NumberTheory/TotientAsymptotic/UntruncatedRemainder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.primeOnly line 11
2. def OAI.TotientAsymptotic.IsUntruncatedRemainder line 13
3. lemma OAI.TotientAsymptotic.primeOnly_prime line 17
4. lemma OAI.TotientAsymptotic.primeOnly_coord line 20
5. lemma OAI.TotientAsymptotic.untruncated_basic line 23
6. lemma OAI.TotientAsymptotic.untruncated_prime_mem line 29
7. lemma OAI.TotientAsymptotic.fordRemainder_untruncated line 33