OAI/NumberTheory/CubicMoment/Theta/CubicThetaWeightFactor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Splitting an unramified primary factor from the actual Eisenstein row weight. Common-factor zeros are retained in every identity.

  1. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_factor line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_mix line 27
  3. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_congr line 44
  4. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_congr_of_eq line 49