OAI/NumberTheory/DirichletL/Descent/SecondSourceAttachment.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.InverseMoment.SecondParentSource line 13
  2. def OAI.SevenEighths.InverseMoment.attachSecondExpansion line 20
  3. def OAI.SevenEighths.InverseMoment.secondParentOf line 30
  4. theorem OAI.SevenEighths.InverseMoment.attachSecondExpansion_injective line 38
  5. theorem OAI.SevenEighths.InverseMoment.attachSecondExpansion_recover line 44
  6. def OAI.SevenEighths.InverseMoment.secondSourceParentEquiv line 50
  7. def OAI.SevenEighths.InverseMoment.secondParentLabel line 61
  8. def OAI.SevenEighths.InverseMoment.secondParentDivisor line 66
  9. def OAI.SevenEighths.InverseMoment.secondParentPuncture line 69
  10. theorem OAI.SevenEighths.InverseMoment.attached_source_conditions line 75
  11. theorem OAI.SevenEighths.InverseMoment.attached_inherited_profile line 107
  12. theorem OAI.SevenEighths.InverseMoment.attached_signed_weight line 113
  13. theorem OAI.SevenEighths.InverseMoment.secondExpansionSource_attached line 121