OAI/NumberTheory/DirichletL/Moments/NaturalPrimitive.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentNaturalPrimitive.redundantSet line 12
2. def OAI.SevenEighths.CenteredMomentNaturalPrimitive.redundantIdeal line 14
3. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.redundantSet_prime line 16
4. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.redundantSet_subset line 19
5. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.prime_mem_support_iff line 22
6. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.mem_redundantSet line 27
7. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.redundantIdeal_squarefree line 36
8. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.redundantIdeal_ne_zero line 39
9. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.redundantIdeal_support line 42
10. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.redundantIdeal_coprime line 47
11. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.primitive_redundant_dvd line 52
12. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.primitive_redundant_norm line 57
13. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.coprime_support_iff line 63
14. lemma OAI.SevenEighths.CenteredMomentNaturalPrimitive.coprime_original_iff line 74
15. theorem OAI.SevenEighths.CenteredMomentNaturalPrimitive.idealCoeff_natural_deletion line 88
16. theorem OAI.SevenEighths.CenteredMomentNaturalPrimitive.polynomial_natural_deletion line 102
17. theorem OAI.SevenEighths.CenteredMomentNaturalPrimitive.exists_natural_primitive line 115