OAI/NumberTheory/OrdinaryCorrelations/HighTrace/LinePrimeMemFullUsed.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.line_prime_mem_fullUsed line 23
2. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.list_prime_mem_fullUsed line 28
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.LineExpression.factors_fullUsed line 34
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.factors_fullUsed line 40
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.used line 55
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.witness_prime_mem_used line 58
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.test_support_used line 63
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.test_factors_used line 75
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.used_card_le line 96
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.usedEmbedding line 100
11. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.usedTestSystem line 108
12. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.usedTestSystem_admissible line 117