OAI/NumberTheory/DirichletL/Moments/SecondSixthSource.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentSecondSixthSource.sixthFactor_span_dvd line 15
  2. theorem OAI.SevenEighths.CenteredMomentSecondSixthSource.fixed_sixth_coefficient line 28
  3. theorem OAI.SevenEighths.CenteredMomentSecondSixthSource.residual_sixth_coefficient line 35
  4. abbrev OAI.SevenEighths.CenteredMomentSecondSixthSource.ActiveIndex line 43
  5. def OAI.SevenEighths.CenteredMomentSecondSixthSource.activePrime line 45
  6. def OAI.SevenEighths.CenteredMomentSecondSixthSource.activeExponent line 48
  7. theorem OAI.SevenEighths.CenteredMomentSecondSixthSource.activeExponent_pos line 51
  8. theorem OAI.SevenEighths.CenteredMomentSecondSixthSource.activeExponent_lt line 56
  9. theorem OAI.SevenEighths.CenteredMomentSecondSixthSource.reducedNumerator_active_product line 59