OAI/NumberTheory/OrdinaryCorrelations/HighTrace/FarTemplate.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate line 20
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.selected line 25
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.root line 26
4. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.first line 27
5. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.second line 29
6. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.expression line 31
7. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.WellFormed line 33
8. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.embedding line 37
9. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.system line 39
10. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.formed_of_relabel line 53
11. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.FarTemplate.card_le line 72
12. abbrev OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.GoodFarTemplate line 93
13. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.farTemplateMass line 94
14. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.farTemplateMass_le line 98