OAI/NumberTheory/DirichletL/Inversion/InitialEnergyCallerPool.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.InverseInitialEnergyCallerPool.residual_factors_in_pool line 15
  2. def OAI.SevenEighths.InverseInitialEnergyCallerPool.forcedSlots line 27
  3. theorem OAI.SevenEighths.InverseInitialEnergyCallerPool.forcedSlots_image line 30
  4. theorem OAI.SevenEighths.InverseInitialEnergyCallerPool.forcedSlots_product line 43
  5. theorem OAI.SevenEighths.InverseInitialEnergyCallerPool.original_selector_forced_slots line 53