OAI/NumberTheory/CubicGram/Conjugation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Eisenstein conjugation, characters and Gauss-sum symmetry.

  1. lemma OAI.CubicFirstMoment.star_omega_linear line 15
  2. lemma OAI.CubicFirstMoment.star_omega line 18
  3. lemma OAI.CubicFirstMoment.star_mem_eisenstein line 22
  4. def OAI.CubicFirstMoment.conjugate line 32
  5. lemma OAI.CubicFirstMoment.conjugate_coe line 40
  6. lemma OAI.CubicFirstMoment.conjugate_conjugate line 42
  7. lemma OAI.CubicFirstMoment.conjugate_omegaE line 45
  8. lemma OAI.CubicFirstMoment.norm_conjugate line 47
  9. lemma OAI.CubicFirstMoment.normNat_conjugate line 50
  10. lemma OAI.CubicFirstMoment.primary_conjugate line 53
  11. lemma OAI.CubicFirstMoment.primaryPrime_conjugate line 58
  12. def OAI.CubicFirstMoment.residueConjugate line 62
  13. lemma OAI.CubicFirstMoment.residueConjugate_mk line 66
  14. lemma OAI.CubicFirstMoment.isUnit_residue_conjugate line 70
  15. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_conjugate line 82
  16. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_unit_cube line 101
  17. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_neg_one line 108
  18. lemma OAI.CubicFirstMoment.cubicSymbolAtPrime_neg line 119
  19. lemma OAI.CubicFirstMoment.additivePhase_conjugate line 124
  20. lemma OAI.CubicFirstMoment.additivePhase_neg line 129
  21. theorem OAI.CubicFirstMoment.gaussAtPrime_conjugate line 135