OAI/NumberTheory/DirichletL/Detector/GramJointFixed.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeGramCommon.primaryCoefficient line 13
2. lemma OAI.SevenEighths.ProbeGramCommon.primaryCoefficient_norm line 16
3. def OAI.SevenEighths.ProbeGramCommon.jointFixedModulus line 23
4. lemma OAI.SevenEighths.ProbeGramCommon.jointFixedModulus_nonzero line 26
5. lemma OAI.SevenEighths.ProbeGramCommon.primaryCoefficient_periodic line 32
6. def OAI.SevenEighths.ProbeGramCommon.jointFixed line 45
7. lemma OAI.SevenEighths.ProbeGramCommon.jointFixed_norm line 51
8. lemma OAI.SevenEighths.ProbeGramCommon.jointFixed_periodic line 61