OAI/NumberTheory/DirichletL/Moments/FirstCanonicalFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalFamily.supported_of_dvd line 17
  2. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalFamily.activeConductor_supported line 22
  3. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalFamily.subsetGenerator_span_dvd line 26
  4. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalFamily.subsetGenerator_supported line 36
  5. def OAI.SevenEighths.CenteredMomentFirstCanonicalFamily.canonicalActiveCharacter line 41
  6. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalFamily.canonicalActiveCharacter_mk line 45
  7. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalFamily.exists_canonical_first_pair line 50
  8. theorem OAI.SevenEighths.CenteredMomentFirstCanonicalFamily.first_displayed_norm line 81