OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeValuation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Unique separation of an unramified prime power in an actual admissible Eisenstein denominator.

  1. abbrev OAI.CubicFirstMoment.CubicThetaDenominator line 11
  2. abbrev OAI.CubicFirstMoment.CubicThetaPrimeFreeDenominator line 12
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimePower_unique line 15
  4. def OAI.CubicFirstMoment.cubicThetaPrimePowerDenominator line 36
  5. theorem OAI.CubicFirstMoment.cubicThetaPrimePowerDenominator_bijective line 41
  6. def OAI.CubicFirstMoment.cubicThetaPrimePowerDenominatorEquiv line 57