OAI/NumberTheory/CubicMoment/Theta/CubicThetaUnitCount.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The six units and the exact index of primary invertible residues.

  1. lemma OAI.CubicFirstMoment.eisenstein_unit_pow_six line 9
  2. lemma OAI.CubicFirstMoment.eisenstein_neg_omega_primitive line 23
  3. def OAI.CubicFirstMoment.eisensteinUnitsEquivSixthRoots line 33
  4. lemma OAI.CubicFirstMoment.eisenstein_units_card line 39
  5. def OAI.CubicFirstMoment.eisensteinUnitReductionThree line 43
  6. lemma OAI.CubicFirstMoment.eisensteinUnitReductionThree_bijective line 46
  7. lemma OAI.CubicFirstMoment.cubicTheta_residue_three_units_card line 75
  8. theorem OAI.CubicFirstMoment.cubicTheta_primaryResidue_six line 79
  9. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_constant_units line 83