OAI/NumberTheory/CubicGram/SquarefreeGauss.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Composite residue characters, Chinese remainders and squarefree Gauss norms.

  1. def OAI.CubicFirstMoment.cubicSymbol line 16
  2. def OAI.CubicFirstMoment.gauss line 19
  3. lemma OAI.CubicFirstMoment.primary_ne_zero line 23
  4. lemma OAI.CubicFirstMoment.primaryNormalize_normalize line 30
  5. lemma OAI.CubicFirstMoment.cubicSymbol_prime line 37
  6. lemma OAI.CubicFirstMoment.gauss_prime line 42
  7. lemma OAI.CubicFirstMoment.cubicSymbol_congr_prime_divisors line 45
  8. lemma OAI.CubicFirstMoment.cubicSymbol_congr line 56
  9. lemma OAI.CubicFirstMoment.gauss_eq_finite_sum line 64
  10. lemma OAI.CubicFirstMoment.exists_primary_prime_square_dvd line 69
  11. lemma OAI.CubicFirstMoment.cubicSymbol_add_last_lift line 81
  12. lemma OAI.CubicFirstMoment.additivePhase_last_lift line 95
  13. lemma OAI.CubicFirstMoment.exists_nontrivial_additivePhase line 105
  14. theorem OAI.CubicFirstMoment.gauss_eq_zero_of_not_squarefree line 112
  15. lemma OAI.CubicFirstMoment.cubicSymbol_mul_lower line 150
  16. lemma OAI.CubicFirstMoment.cubicSymbol_mul_upper line 154
  17. lemma OAI.CubicFirstMoment.residue_eq_of_dvd_sub line 165
  18. def OAI.CubicFirstMoment.residueMix line 169
  19. lemma OAI.CubicFirstMoment.residueMix_injective line 173
  20. lemma OAI.CubicFirstMoment.residueMix_bijective line 195
  21. lemma OAI.CubicFirstMoment.additivePhase_mix line 209
  22. lemma OAI.CubicFirstMoment.cubicSymbol_mix line 227
  23. theorem OAI.CubicFirstMoment.gauss_mul_of_isCoprime line 241
  24. lemma OAI.CubicFirstMoment.residue_isUnit_of_isCoprime line 283
  25. lemma OAI.CubicFirstMoment.norm_cubicSymbolAtPrime_of_isCoprime line 290
  26. lemma OAI.CubicFirstMoment.norm_cubicSymbol_of_isCoprime line 297
  27. lemma OAI.CubicFirstMoment.gauss_one line 311
  28. lemma OAI.CubicFirstMoment.primaryPrimes_isCoprime line 321
  29. lemma OAI.CubicFirstMoment.norm_gauss_prod_primaryPrimes line 328
  30. theorem OAI.CubicFirstMoment.norm_gauss_of_squarefree line 346
  31. theorem OAI.CubicFirstMoment.norm_gauss line 351