OAI/NumberTheory/CubicMoment/Theta/CubicThetaCommonSupport.lean
3 declarations, 0 contain sorry, 0 declared as axioms
The actual three-cusp coefficient has squarefree-times-cube support. This is proved for the constructed cusps, including their ramified shifts.
- lemma
OAI.CubicFirstMoment.cubicThetaArithmetic_zero_of_no_primary_coordinatesline 13 - lemma
OAI.CubicFirstMoment.cubicThetaCommon_zero_of_no_primary_coordinatesline 22 - theorem
OAI.CubicFirstMoment.cubicThetaCommonCuspCoefficient_supportline 47