OAI/NumberTheory/OrdinaryCorrelations/HighTrace/NumericalLine.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine line 20
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.toEmpty line 25
3. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.toEmpty_injective line 28
4. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.(instance at line 37) line 37
5. instance OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.(instance at line 38) line 38
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.listEquiv line 40
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.listEquiv_eval line 47
8. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.sum_sigma_instances line 53
9. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.sum_lists line 60
10. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.sourceRetained line 74
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.NumericalLine.retained_list_sum_le line 79