OAI/NumberTheory/DirichletL/Detector/GramLocalExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeGramCommon.finiteField_local_norm line 13
2. def OAI.SevenEighths.ProbeGramCommon.localExtension line 22
3. lemma OAI.SevenEighths.ProbeGramCommon.localExtension_both_zero line 30
4. theorem OAI.SevenEighths.ProbeGramCommon.localExtension_periodic line 34
5. theorem OAI.SevenEighths.ProbeGramCommon.localExtension_norm line 47
6. theorem OAI.SevenEighths.ProbeGramCommon.primePower_common_extension line 69