OAI/NumberTheory/DirichletL/Inversion/InitialExcludedPolynomial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseInitialExcludedPolynomial.prime_product_squarefree line 14
2. theorem OAI.SevenEighths.InverseInitialExcludedPolynomial.deleted_coefficient_product line 23
3. theorem OAI.SevenEighths.InverseInitialExcludedPolynomial.residual_source line 30
4. theorem OAI.SevenEighths.InverseInitialExcludedPolynomial.source_decomposition line 61
5. theorem OAI.SevenEighths.InverseInitialExcludedPolynomial.polynomial_all_ideals line 78
6. theorem OAI.SevenEighths.InverseInitialExcludedPolynomial.scale_normalization line 99
7. theorem OAI.SevenEighths.InverseInitialExcludedPolynomial.inverse_polynomial_decomposition line 104