OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedRowInflation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Reduce every ramified row to one fixed residue ring. Only three ramified exponents remain in its weight; the frequency and primary part are retained exactly.

  1. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_lambda_mod line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_ramified_mod line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_ramified_congr line 31
  4. def OAI.CubicFirstMoment.cubicThetaRamifiedBaseRow line 39
  5. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_ramified_inflation line 48