OAI/NumberTheory/DirichletL/Detector/GramIdealDilation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.ProbeGramCommon.DivisibleSupported line 12
2. def OAI.SevenEighths.ProbeGramCommon.supportedIdealProduct line 14
3. def OAI.SevenEighths.ProbeGramCommon.supportedDilationEquiv line 17
4. lemma OAI.SevenEighths.ProbeGramCommon.supported_dilation_generator line 28
5. lemma OAI.SevenEighths.ProbeGramCommon.supported_dilation_norm line 32
6. theorem OAI.SevenEighths.ProbeGramCommon.supported_divisor_tsum line 36
7. theorem OAI.SevenEighths.ProbeGramCommon.supported_divisor_pair_tsum line 43