OAI/NumberTheory/DirichletL/Descent/SecondSquarefree.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.sourceIdeal_squarefree line 19
2. theorem OAI.SevenEighths.InverseMoment.sourceIdeal_coprime_of_disjoint line 29
3. lemma OAI.SevenEighths.InverseMoment.prime_span_coprime_of_not_mem line 39
4. theorem OAI.SevenEighths.InverseMoment.sourceIdeal_coprime_of_not_mem line 50
5. theorem OAI.SevenEighths.InverseMoment.jLabel_span_dvd_source line 57
6. theorem OAI.SevenEighths.InverseMoment.secondInputCoefficient_zero_of_label_mem line 66
7. theorem OAI.SevenEighths.InverseMoment.secondPreColumn_zero_of_mask_label_mem line 74
8. theorem OAI.SevenEighths.InverseMoment.secondSignedSourceWeight_nonzero_masks line 86
9. def OAI.SevenEighths.InverseMoment.actualSecondSignedWeight line 118
10. theorem OAI.SevenEighths.InverseMoment.actualSecondSignedWeight_norm_le_one line 127
11. theorem OAI.SevenEighths.InverseMoment.actual_second_nonzero_weight_squarefree line 134