OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedAllRows.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The explicit finite ramified factor for all six global units.

  1. theorem OAI.CubicFirstMoment.cubicThetaUnit_signed_power line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaNorm_lambda_pow line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaNorm_unit_lambda_pow line 19
  4. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_all_ramified line 23
  5. theorem OAI.CubicFirstMoment.cubicThetaRamifiedFactor_value line 38