OAI/NumberTheory/DirichletL/Detector/GramIdealMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeGramCommon.normalized_double_sum_bound line 13
2. theorem OAI.SevenEighths.ProbeGramCommon.canonical_nonexceptional_ideal_sum line 30
3. theorem OAI.SevenEighths.ProbeGramCommon.canonical_exceptional_ideal_sum line 85