OAI/NumberTheory/DirichletL/Descent/SecondCanonicalChild.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseMoment.primaryGenerator_primeProduct line 21
2. def OAI.SevenEighths.InverseMoment.actualSecondPuncture line 37
3. def OAI.SevenEighths.InverseMoment.actualSecondRawLabel line 40
4. theorem OAI.SevenEighths.InverseMoment.finiteCanonicalMarkedRow_mask_span line 46
5. theorem OAI.SevenEighths.InverseMoment.actual_second_puncture_span line 53
6. theorem OAI.SevenEighths.InverseMoment.actual_second_generator_sectors line 72
7. theorem OAI.SevenEighths.InverseMoment.actual_second_canonical_child line 109