OAI/NumberTheory/DirichletL/Detector/GramNonzeroFrequency.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeGramCommon.nonzero_tsum_indicator line 12
2. def OAI.SevenEighths.ProbeGramCommon.gramFrequencyNeg line 22
3. lemma OAI.SevenEighths.ProbeGramCommon.actual_common_nonzero_tsum line 28
4. lemma OAI.SevenEighths.ProbeGramCommon.actual_gcd_nonzero_frequency_source line 40