OAI/NumberTheory/CubicGram/ResidueCharacters.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Primitive cube roots, Euler residue characters and additive trace phases.

  1. lemma OAI.CubicFirstMoment.omega_cube line 14
  2. lemma OAI.CubicFirstMoment.omegaE_quadratic line 17
  3. lemma OAI.CubicFirstMoment.omegaE_cube line 21
  4. lemma OAI.CubicFirstMoment.omegaE_difference_product line 25
  5. lemma OAI.CubicFirstMoment.primaryPrime_not_dvd_three line 28
  6. lemma OAI.CubicFirstMoment.residue_omega_primitive line 35
  7. lemma OAI.CubicFirstMoment.primaryPrime_norm_sub_one_dvd_three line 50
  8. lemma OAI.CubicFirstMoment.cubicSymbol_euler_exists_unique line 62
  9. lemma OAI.CubicFirstMoment.residueRepresentative_spec line 83

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

  10. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_congr line 87
  11. lemma OAI.CubicFirstMoment.trace_ofCoords line 92
  12. lemma OAI.CubicFirstMoment.trace_integral line 99
  13. lemma OAI.CubicFirstMoment.additivePhase_add_multiple line 103
  14. lemma OAI.CubicFirstMoment.additivePhase_congr line 124
  15. lemma OAI.CubicFirstMoment.gaussAtPrime_eq_finite_sum line 135