OAI/NumberTheory/CubicGram/GaussCharacters.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative and additive characters and normalized prime Gauss sums.

  1. lemma OAI.CubicFirstMoment.cube_pow_mod line 14
  2. lemma OAI.CubicFirstMoment.cubicSymbol_euler_value line 19
  3. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_one line 29
  4. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_mul line 35
  5. def OAI.CubicFirstMoment.cubicResidueChar line 65
  6. lemma OAI.CubicFirstMoment.cubicResidueChar_mk line 82
  7. lemma OAI.CubicFirstMoment.additivePhase_add line 86
  8. lemma OAI.CubicFirstMoment.additivePhase_zero line 98
  9. def OAI.CubicFirstMoment.residueAddChar line 101
  10. lemma OAI.CubicFirstMoment.residueAddChar_mk line 116
  11. lemma OAI.CubicFirstMoment.gaussAtPrime_eq_gaussSum line 120
  12. lemma OAI.CubicFirstMoment.omega_primitive line 126
  13. lemma OAI.CubicFirstMoment.cubicResidueChar_ne_one line 135
  14. lemma OAI.CubicFirstMoment.omega_star line 171
  15. lemma OAI.CubicFirstMoment.trace_pair_lattice line 175
  16. lemma OAI.CubicFirstMoment.additivePhase_eq_one_iff line 182
  17. lemma OAI.CubicFirstMoment.residueAddChar_ne_one line 196
  18. lemma OAI.CubicFirstMoment.norm_gaussAtPrime line 214