OAI/NumberTheory/CubicGram/Jacobi.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Cubic Jacobi sums and the prime Gauss cube identity.

  1. lemma OAI.CubicFirstMoment.cubicResidueChar_cube line 16
  2. lemma OAI.CubicFirstMoment.cubicResidueChar_order line 25
  3. lemma OAI.CubicFirstMoment.cubicResidueChar_mem line 30
  4. def OAI.CubicFirstMoment.cubicResidueCharE line 38
  5. lemma OAI.CubicFirstMoment.cubicResidueCharE_coe line 45
  6. lemma OAI.CubicFirstMoment.cubicResidueCharE_euler line 48
  7. def OAI.CubicFirstMoment.primeJacobi line 75
  8. lemma OAI.CubicFirstMoment.primeJacobi_coe line 80
  9. lemma OAI.CubicFirstMoment.primeJacobi_primary line 91
  10. lemma OAI.CubicFirstMoment.primeJacobi_dvd line 109
  11. lemma OAI.CubicFirstMoment.gaussAtPrime_cube_jacobi line 141
  12. lemma OAI.CubicFirstMoment.norm_primeJacobi line 168
  13. lemma OAI.CubicFirstMoment.isUnit_of_norm_eq_one line 181
  14. lemma OAI.CubicFirstMoment.primeJacobi_eq_neg line 189
  15. theorem OAI.CubicFirstMoment.gaussAtPrime_cube line 205