OAI/NumberTheory/OrdinaryCorrelations/HighTrace/IntegerResidues.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.integerResidues line 16
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.modulus line 18
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.modulus_pos line 20
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.prime_dvd_modulus line 23
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.integerResidues_periodic line 26
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.residue_surjective line 37
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.residues_card line 60
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.residueEquiv line 63
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.period_mean line 68