OAI/NumberTheory/CubicMoment/Angular/AngularPrimeInputsProof.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Both literal angular prime inputs follow from the published primitive angular Hecke completion. Their original conductor majorants are preserved.

  1. theorem OAI.CubicFirstMoment.fixedAngularPrimeExplicitEstimate_of_primitive line 12
  2. theorem OAI.CubicFirstMoment.angularKummerPrimeExplicitEstimate_of_primitive line 37