OAI/NumberTheory/CubicMoment/Theta/CubicThetaResidueLocalCoefficient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The concrete finite dual cusp coefficient equals the universal three-cusp coefficient times the exact local Ramanujan product.

  1. theorem OAI.CubicFirstMoment.cubicThetaResidueDualCoefficient_local line 13