OAI/NumberTheory/DirichletL/Moments/SecondChildProfile.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentSecondChildProfile.child_ideal_primary line 16
  2. theorem OAI.SevenEighths.CenteredMomentSecondChildProfile.exists_second_height_character line 27
  3. theorem OAI.SevenEighths.CenteredMomentSecondChildProfile.second_divisor_column line 45