OAI/NumberTheory/DirichletL/Inversion/InitialEnergyCallerSelector.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.InverseInitialEnergyCallerSelector.mask_nonzero_coprimeline 15 - theorem
OAI.SevenEighths.InverseInitialEnergyCallerSelector.reconstructedSelector_profileline 37 - theorem
OAI.SevenEighths.InverseInitialEnergyCallerSelector.singleton_primeMarkline 63 - theorem
OAI.SevenEighths.InverseInitialEnergyCallerSelector.forcing_primeMarkline 76 - theorem
OAI.SevenEighths.InverseInitialEnergyCallerSelector.reconstructedSelector_forced_markline 92