OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Ordered.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Case.ordered line 26
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Case.ordered_precedes line 31
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.modulus_mem line 39
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.modulus_eq_selected line 44
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.testEmbedding line 51
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.testSystem line 57
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.testSize line 76
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.testSize_nonneg line 79
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Test.log_symbolic_size line 84
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.testSystem_admissible line 93