OAI/NumberTheory/CubicGram/EuclideanDomain.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Nearest-lattice division and the Eisenstein Euclidean domain.

  1. lemma OAI.CubicFirstMoment.normNat_mul line 14
  2. lemma OAI.CubicFirstMoment.normNat_one line 19
  3. lemma OAI.CubicFirstMoment.normNat_zero line 24
  4. lemma OAI.CubicFirstMoment.real_coordinates_norm line 29

    Also declared: OAI/NumberTheory/CubicGauss/Eisenstein.lean:19 (same declaration text).

  5. def OAI.CubicFirstMoment.nearestEisenstein line 37
  6. lemma OAI.CubicFirstMoment.complex_coordinates line 40

    Also declared: OAI/NumberTheory/CubicGauss/Eisenstein.lean:27 (same declaration text).

  7. lemma OAI.CubicFirstMoment.nearestEisenstein_normSq_lt line 52
  8. lemma OAI.CubicFirstMoment.nearestEisenstein_zero line 70
  9. def OAI.CubicFirstMoment.latticeQuotient line 73
  10. def OAI.CubicFirstMoment.latticeRemainder line 76
  11. lemma OAI.CubicFirstMoment.normNat_latticeRemainder_lt line 78
  12. instance OAI.CubicFirstMoment.eisensteinEuclideanDomain line 90
  13. instance OAI.CubicFirstMoment.eisensteinNormalization line 105
  14. def OAI.CubicFirstMoment.normNatHom line 108
  15. lemma OAI.CubicFirstMoment.associated_normNat line 113