OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Spec.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.spec line 25
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.expression line 29
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.expression_eval line 32
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.expression_support line 38
5. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection line 48
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.selection_exists line 57
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.embedding line 63
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.tests line 65
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.coefficient_not_dvd line 79
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GapFamily.Selection.admissible line 85