OAI/NumberTheory/DirichletL/Descent/SecondParentInput.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.secondInputCoefficient_old_divisor_mask line 17
2. theorem OAI.SevenEighths.InverseMoment.inputConjugateRow_old_divisor_mask line 31
3. theorem OAI.SevenEighths.InverseMoment.inputConjugateRow_puncture_span line 36
4. theorem OAI.SevenEighths.InverseMoment.fresh_input_parent_mask line 42
5. theorem OAI.SevenEighths.InverseMoment.first_fresh_parent_truncated line 64