OAI/NumberTheory/CubicGram/IntegerBasis.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The integral basis, multiplication norm and finite residue quotients.

  1. def OAI.CubicFirstMoment.coordinatesMap line 14
  2. lemma OAI.CubicFirstMoment.coordinatesMap_bijective line 19
  3. def OAI.CubicFirstMoment.coordinatesEquiv line 31
  4. def OAI.CubicFirstMoment.integerBasis line 34
  5. instance OAI.CubicFirstMoment.(instance at line 37) line 37
  6. instance OAI.CubicFirstMoment.(instance at line 38) line 38
  7. lemma OAI.CubicFirstMoment.integerBasis_zero line 40
  8. lemma OAI.CubicFirstMoment.integerBasis_one line 43
  9. lemma OAI.CubicFirstMoment.integerBasis_repr_ofCoords line 46
  10. lemma OAI.CubicFirstMoment.ofCoords_mul line 54
  11. lemma OAI.CubicFirstMoment.ofCoords_mul_omega line 65
  12. lemma OAI.CubicFirstMoment.leftMulMatrix_ofCoords line 69
  13. lemma OAI.CubicFirstMoment.algebra_norm_ofCoords line 75
  14. lemma OAI.CubicFirstMoment.algebra_norm_cast line 81
  15. lemma OAI.CubicFirstMoment.residues_card line 85
  16. lemma OAI.CubicFirstMoment.norm_eq_zero_iff line 106
  17. lemma OAI.CubicFirstMoment.normNat_ne_zero line 113
  18. lemma OAI.CubicFirstMoment.finite_residues line 119