OAI/NumberTheory/CubicGram/Coordinates.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Integral coordinates and finite norm cutoffs in the Eisenstein subring.

  1. lemma OAI.CubicFirstMoment.omega_eq line 14
  2. lemma OAI.CubicFirstMoment.omega_re line 30
  3. lemma OAI.CubicFirstMoment.omega_im line 31
  4. lemma OAI.CubicFirstMoment.omega_quadratic line 33
  5. lemma OAI.CubicFirstMoment.exists_coordinates line 38
  6. lemma OAI.CubicFirstMoment.coordinates_norm line 58
  7. lemma OAI.CubicFirstMoment.coordinates_unique line 65
  8. lemma OAI.CubicFirstMoment.norm_nonneg line 77
  9. lemma OAI.CubicFirstMoment.normNat_cast line 79
  10. def OAI.CubicFirstMoment.ofCoords line 88
  11. lemma OAI.CubicFirstMoment.ofCoords_coe line 90
  12. lemma OAI.CubicFirstMoment.ofCoords_surjective line 92
  13. lemma OAI.CubicFirstMoment.ofCoords_injective line 97
  14. lemma OAI.CubicFirstMoment.finite_norm_le line 102
  15. def OAI.CubicFirstMoment.primeCutoff line 126
  16. lemma OAI.CubicFirstMoment.mem_primeCutoff line 131
  17. lemma OAI.CubicFirstMoment.primeCutoffSum_eq_sum line 134