OAI/NumberTheory/DirichletL/Detector/GramCommonParam.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.ProbeGramCommon.ResidueQ line 10
2. def OAI.SevenEighths.ProbeGramCommon.condition line 12
3. abbrev OAI.SevenEighths.ProbeGramCommon.Solutions line 17
4. def OAI.SevenEighths.ProbeGramCommon.leftParam line 19
5. def OAI.SevenEighths.ProbeGramCommon.rightParam line 22
6. lemma OAI.SevenEighths.ProbeGramCommon.leftParam_mk line 26
7. lemma OAI.SevenEighths.ProbeGramCommon.rightParam_mk line 31
8. lemma OAI.SevenEighths.ProbeGramCommon.param_condition line 36
9. def OAI.SevenEighths.ProbeGramCommon.param line 46
10. lemma OAI.SevenEighths.ProbeGramCommon.param_injective line 49
11. lemma OAI.SevenEighths.ProbeGramCommon.condition_divided line 56
12. lemma OAI.SevenEighths.ProbeGramCommon.param_surjective line 64
13. def OAI.SevenEighths.ProbeGramCommon.solutionEquiv line 95
14. lemma OAI.SevenEighths.ProbeGramCommon.solutionEquiv_val line 100