OAI/NumberTheory/OrdinaryCorrelations/HighTrace/DivisorFamily.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.DivisorFamily line 14
2. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification line 26
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.QualifiesAt line 47
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.primeSupport line 50
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.ResidueTest line 53
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.OrientedSubpath line 58
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.Primitive line 67
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.squarefree_int_dvd_iff line 77
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.qualifies_iff_residueTests line 90
10. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.TraceVertices line 117
11. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec line 119
12. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.AttachedSpec.vertex line 124
13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listLocal line 127
14. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listIndicator line 131
15. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listIndicator_product line 135
16. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.listLocal_nonneg line 153