OAI/NumberTheory/CubicGauss/HeckeIdeals.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Principal ideals, unit orbits and ideal-theoretic Hecke series.

  1. lemma OAI.CubicFirstMoment.normNat_of_isUnit line 16

    Also declared: OAI/NumberTheory/CubicGram/PrimaryNormalization.lean:16 (same declaration text).

  2. lemma OAI.CubicFirstMoment.norm_of_isUnit line 19

    Also declared: OAI/NumberTheory/CubicGram/PrimaryNormalization.lean:19 (same declaration text).

  3. lemma OAI.CubicFirstMoment.HeckeTheta.norm_ofCoords_eq_one_iff line 24
  4. lemma OAI.CubicFirstMoment.HeckeTheta.norm_one_isUnit line 29
  5. def OAI.CubicFirstMoment.HeckeTheta.sixUnitCoords line 38
  6. lemma OAI.CubicFirstMoment.HeckeTheta.mem_sixUnitCoords line 41
  7. def OAI.CubicFirstMoment.HeckeTheta.sixUnitsEquiv line 57
  8. instance OAI.CubicFirstMoment.HeckeTheta.(instance at line 75) line 75
  9. lemma OAI.CubicFirstMoment.HeckeTheta.card_eisenstein_units line 77
  10. lemma OAI.CubicFirstMoment.HeckeTheta.ideal_generator_ne_zero line 83
  11. def OAI.CubicFirstMoment.HeckeTheta.modulusFiberEquiv line 86
  12. lemma OAI.CubicFirstMoment.HeckeTheta.tsum_elements_eq_six_ideal_generators line 103
  13. def OAI.CubicFirstMoment.HeckeTheta.TrivialInfinity line 128
  14. lemma OAI.CubicFirstMoment.HeckeTheta.norm_mul_unit line 131
  15. def OAI.CubicFirstMoment.HeckeTheta.idealNorm line 137
  16. lemma OAI.CubicFirstMoment.HeckeTheta.idealNorm_generator line 139
  17. def OAI.CubicFirstMoment.HeckeTheta.idealHeckeSeries line 144
  18. theorem OAI.CubicFirstMoment.HeckeTheta.elementHeckeSeries_eq_idealSeries line 148
  19. theorem OAI.CubicFirstMoment.HeckeTheta.idealHeckeSeries_eq_nonzero_idealSum line 170
  20. lemma OAI.CubicFirstMoment.HeckeTheta.ideal_coefficient_eq_of_generator line 185
  21. lemma OAI.CubicFirstMoment.HeckeTheta.inverse_character_eq_conjugate line 197
  22. lemma OAI.CubicFirstMoment.HeckeTheta.TrivialInfinity.inv line 203
  23. def OAI.CubicFirstMoment.HeckeTheta.conductorScale line 208
  24. lemma OAI.CubicFirstMoment.HeckeTheta.conductorScale_pos line 210
  25. def OAI.CubicFirstMoment.HeckeTheta.analyticHeckeL line 214
  26. theorem OAI.CubicFirstMoment.HeckeTheta.analyticHeckeL_entire line 217
  27. theorem OAI.CubicFirstMoment.HeckeTheta.analyticHeckeL_eq_idealSeries line 225
  28. theorem OAI.CubicFirstMoment.HeckeTheta.exact_completion_identity line 239
  29. theorem OAI.CubicFirstMoment.HeckeTheta.primitive_Hecke_analytic_input line 249