OAI/NumberTheory/DirichletL/Detector/CentralRepeatedChoices.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeCentralRepeatedChoices.activeChoices line 12
2. lemma OAI.SevenEighths.ProbeCentralRepeatedChoices.active_card_le_divisors line 17
3. theorem OAI.SevenEighths.ProbeCentralRepeatedChoices.active_card_subpower line 35
4. lemma OAI.SevenEighths.ProbeCentralRepeatedChoices.sum_products_restrict line 67