OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedPrimaryFactor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Separate the primary part of every actual ramified row. Reciprocity reduces its correction to one explicit finite character squared.

  1. lemma OAI.CubicFirstMoment.cubicThetaRamifiedPrimaryPhase line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_ramified_primary line 26