OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedDenominator.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Unique ramified coordinates for exactly the admissible Eisenstein denominators. The exponent starts at two because the rows are divisible by three. Global units are retained.

  1. abbrev OAI.CubicFirstMoment.CubicThetaPrimaryPart line 13
  2. def OAI.CubicFirstMoment.cubicThetaRamifiedDenominator line 15
  3. theorem OAI.CubicFirstMoment.cubicThetaRamifiedDenominator_bijective line 24
  4. def OAI.CubicFirstMoment.cubicThetaRamifiedDenominatorEquiv line 52