OAI/NumberTheory/CubicMoment/Theta/CubicThetaGaussTwist.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identification of the normalized Gauss factor in the literal cubic theta coefficient formula with its finite additive-frequency sum.

  1. def OAI.CubicFirstMoment.cubicThetaFiniteGauss line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaFiniteGauss_eq line 18

    Source documentation

    Multiplication by the invertible additive frequency permutes the residue ring; no primitive character or analytic input is needed.

    theorem cubicThetaFiniteGauss_eq {c α : Eisenstein} (hc : primary c)
    (hα : IsCoprime c α) : cubicThetaFiniteGauss c α = cubicThetaTwistedGauss c α := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicThetaFiniteGauss, OAI.CubicFirstMoment.cubicThetaTwistedGauss