OAI/NumberTheory/DirichletL/Moments/FirstCanonicalAllowance.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalAllowance.activeConductor_span_product line 16
  2. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalAllowance.active_generator_ideal_product line 24
  3. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalAllowance.common_ideal_product line 31
  4. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalAllowance.common_generator_ideal_product line 35
  5. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalAllowance.commonRadical_active_principal line 40
  6. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalAllowance.actual_canonical_common_support_allowance line 50
  7. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalAllowance.activeConductor_span_filter line 67
  8. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalAllowance.extracted_activeConductor_span line 78
  9. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalAllowance.actual_extracted_common_support_allowance line 94