OAI/NumberTheory/DirichletL/Descent/CanonicalChildSupport.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.InverseMoment.canonical_source_prime_supportedline 18 - lemma
OAI.SevenEighths.InverseMoment.canonical_supported_prodline 27 - lemma
OAI.SevenEighths.InverseMoment.canonical_source_ideal_supportedline 43 - lemma
OAI.SevenEighths.InverseMoment.canonical_prime_product_supportedline 49 - lemma
OAI.SevenEighths.InverseMoment.actual_second_label_supportedline 57 - theorem
OAI.SevenEighths.InverseMoment.actual_cell_labels_supportedline 67 - theorem
OAI.SevenEighths.InverseMoment.actual_cell_labels_admissibleline 74