OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedSeries.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact ramified local factor of the normalized totient series.

  1. def OAI.CubicFirstMoment.cubicThetaRamifiedDensitySeries line 9
  2. lemma OAI.CubicFirstMoment.cubicTheta_ramified_denominator_ne_zero line 12
  3. theorem OAI.CubicFirstMoment.cubicThetaRamifiedDensitySeries_eq line 25