OAI/NumberTheory/DirichletL/Detector/GramCanonical.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.ProbeGramCommon.GramFrequency line 15
2. abbrev OAI.SevenEighths.ProbeGramCommon.GramPrime line 16
3. def OAI.SevenEighths.ProbeGramCommon.gramPrime line 17
4. instance OAI.SevenEighths.ProbeGramCommon.gramPrimeMaximal line 18
5. def OAI.SevenEighths.ProbeGramCommon.gramExponent line 21
6. lemma OAI.SevenEighths.ProbeGramCommon.gramExponent_pos line 22
7. lemma OAI.SevenEighths.ProbeGramCommon.gramPrime_good line 24
8. lemma OAI.SevenEighths.ProbeGramCommon.gramPrime_coprime line 26
9. lemma OAI.SevenEighths.ProbeGramCommon.gramPrime_product line 29
10. instance OAI.SevenEighths.ProbeGramCommon.gramPrimePowerFinite line 35
11. instance OAI.SevenEighths.ProbeGramCommon.gramPrimePowerFintype line 38
12. instance OAI.SevenEighths.ProbeGramCommon.gramProductFinite line 40
13. instance OAI.SevenEighths.ProbeGramCommon.gramProductFintype line 44
14. structure OAI.SevenEighths.ProbeGramCommon.GramNumeratorData line 46
15. lemma OAI.SevenEighths.ProbeGramCommon.gramNumeratorData_nonempty line 55
16. def OAI.SevenEighths.ProbeGramCommon.gramNumeratorData line 58
17. def OAI.SevenEighths.ProbeGramCommon.canonicalJoint line 60
18. lemma OAI.SevenEighths.ProbeGramCommon.canonicalJoint_norm line 66