OAI/NumberTheory/DirichletL/MeanSquare/OutsideIdeals.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InitialMeanSquare.idealRowSum_filter_squarefree line 78
  2. def OAI.InitialMeanSquare.outsideSquarefreeIdeals line 104
  3. theorem OAI.InitialMeanSquare.outsideSquarefree_admissible line 107
  4. theorem OAI.InitialMeanSquare.outside_good line 120
  5. theorem OAI.InitialMeanSquare.outside_pool_product_not_dvd line 127
  6. theorem OAI.InitialMeanSquare.selectedIdealTest_outside line 139
  7. theorem OAI.InitialMeanSquare.outside_idealRowSum_initial_energy line 161