OAI/NumberTheory/OrdinaryCorrelations/HighTrace/VertexAt.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.vertexAt line 18
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.edgeAt line 21
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.coefficientAt line 24
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.coefficient line 29
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.edgeAt_eq line 32
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.displacement_eq_sum line 38
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.mul_coefficient_interval line 47
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.Specification.coefficient_restrict line 64