OAI/NumberTheory/CubicMoment/Theta/CubicThetaCoefficientMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact Dirichlet mass of the literal theta coefficients. The unit, ramified, squarefree and cube factors are kept separate.

  1. def OAI.CubicFirstMoment.cubicThetaCoefficientMassTerm line 12
  2. def OAI.CubicFirstMoment.cubicThetaCoefficientMass line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaCoefficientMass_reindex line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaCoordinates_norm line 28
  5. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.mass_term line 37