OAI/NumberTheory/CubicMoment/Theta/CubicThetaInverseResidues.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The inverse residues arising from determinant-one cusp lifts permute the actual unit group. No distribution or cancellation estimate is assumed.

  1. def OAI.CubicFirstMoment.cubicThetaNineConductorUnit line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaNineConductorUnit_val line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaUnitRepresentative_coprime line 23
  4. def OAI.CubicFirstMoment.cubicThetaNineUnitInverse line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaNineUnitInverse_spec line 33
  6. lemma OAI.CubicFirstMoment.cubicThetaNineUnitInverse_residue line 39
  7. theorem OAI.CubicFirstMoment.cubicThetaNineUnitInverse_average line 61