OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedUnitConductor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The ramified conductor cutoff for every global-unit class in the literal denominator decomposition.

  1. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_unit_lambda line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_unit_lambda_periodic line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_full_ramified_periodic line 40
  4. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_full_ramified_support line 52
  5. theorem OAI.CubicFirstMoment.cubicThetaRamifiedTerm_high line 87