OAI/NumberTheory/CubicMoment/Estimates/IdealThetaLattice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact ideal-to-element reindexing for a unit-invariant residue theta series.

  1. lemma OAI.CubicFirstMoment.idealTheta_units_finite line 12
  2. lemma OAI.CubicFirstMoment.idealExponentOf_unit_mul line 17
  3. lemma OAI.CubicFirstMoment.idealElementCoordinates_bijective line 25
  4. def OAI.CubicFirstMoment.idealElementCoordinates line 46
  5. lemma OAI.CubicFirstMoment.idealElementCoordinates_norm line 49
  6. lemma OAI.CubicFirstMoment.residue_char_unit_mul line 56
  7. lemma OAI.CubicFirstMoment.idealTheta_lattice line 64