OAI/NumberTheory/CubicMoment/Angular/AngularNumeratorConductor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Primitive reduction for the literal angular numerator character, with the original 9*v modulus and its exact analytic conductor bound.

  1. theorem OAI.CubicFirstMoment.angularNumerator_primitive_conductor line 11
  2. lemma OAI.CubicFirstMoment.angularNumerator_conductor_bound line 30