OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedCoefficientScaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Ramified cube scaling agrees with the normalization of the published arithmetic coefficient on every positive ramified order.

  1. theorem OAI.CubicFirstMoment.cubicThetaNormalizedObservedCoefficient_lambda_cube line 10
  2. def OAI.CubicFirstMoment.CubicThetaCoordinates.mulLambdaCube line 20
  3. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.amplitude_mulLambdaCube line 35
  4. theorem OAI.CubicFirstMoment.CubicThetaCoordinates.coefficient_mulLambdaCube line 43