OAI/NumberTheory/DirichletL/Moments/RadicalFamily.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentRadicalFamily.elementCoeff_power_pos line 14
2. theorem OAI.SevenEighths.CenteredMomentRadicalFamily.exists_product_presentation line 22
3. theorem OAI.SevenEighths.CenteredMomentRadicalFamily.single_row_on_base line 38
4. theorem OAI.SevenEighths.CenteredMomentRadicalFamily.row_product_formula line 57
5. theorem OAI.SevenEighths.CenteredMomentRadicalFamily.exists_radical_row_presentation line 75