OAI/NumberTheory/DirichletL/GaussSum/SquarePhaseFactorization.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ActualEisensteinCubic.primary_associated_eq line 72
  2. theorem OAI.ActualEisensteinCubic.primary_multiset_prod line 84
  3. theorem OAI.ActualEisensteinCubic.primary_maximal_divisor_good line 96
  4. theorem OAI.ActualEisensteinCubic.exists_primary_prime_factorization line 106
  5. theorem OAI.ActualEisensteinCubic.residue_char_mem line 145
  6. theorem OAI.ActualEisensteinCubic.maximal_eq_or_eq_of_same_residue_char line 151
  7. theorem OAI.ActualEisensteinCubic.prime_divisor_residue_char_ne line 166
  8. theorem OAI.ActualEisensteinCubic.lambda_sq_dvd_three line 176
  9. theorem OAI.ActualEisensteinCubic.neg_two_primary line 186
  10. theorem OAI.ActualEisensteinCubic.neg_add_primary line 189
  11. theorem OAI.ActualEisensteinCubic.prime_generator_not_mem_of_ne line 195
  12. theorem OAI.ActualEisensteinCubic.cubic_reciprocity_equal_residue_char line 205
  13. theorem OAI.ActualEisensteinCubic.cubic_reciprocity_primary line 274
  14. theorem OAI.ActualEisensteinCubic.canonicalSextic_sq_reciprocity_primary line 292
  15. def OAI.ActualEisensteinCubic.cubicTwoIdeal line 309
  16. instance OAI.ActualEisensteinCubic.cubicTwoIdeal_isMaximal line 311
  17. theorem OAI.ActualEisensteinCubic.cubicTwoIdeal_good line 321
  18. theorem OAI.ActualEisensteinCubic.cubicTwoIdeal_residue_char line 325
  19. theorem OAI.ActualEisensteinCubic.canonicalSextic_four_eq_fixed_two line 336
  20. theorem OAI.ActualEisensteinCubic.canonicalSextic_four_prod_eq_fixed_two line 352
  21. theorem OAI.ActualEisensteinCubic.canonicalSextic_four_prod_eq_one_of_mod_two line 365
  22. theorem OAI.IdealGaussCRT.sum_square_phase_finite_crt line 386
  23. theorem OAI.IdealGaussCRT.quadratic_gauss_finite_crt_eq_square_sum line 403
  24. abbrev OAI.QuadraticGaussRay.O line 424
  25. theorem OAI.QuadraticGaussRay.canonicalProductGauss_three_eq_quadraticGamma line 427
  26. theorem OAI.QuadraticGaussRay.I_zpow_eq_of_mod_four line 453
  27. theorem OAI.QuadraticGaussRay.fourTerms_eq_of_mod_four line 460
  28. def OAI.QuadraticGaussRay.quadraticRayValue line 470
  29. theorem OAI.QuadraticGaussRay.quadraticGammaO_eq_rayValue line 473
  30. theorem OAI.QuadraticGaussRay.quadraticGammaO_eq_of_residue_eq line 482
  31. theorem OAI.QuadraticGaussRay.canonicalProductGauss_three_eq_rayValue line 486
  32. theorem OAI.QuadraticGaussRay.fixed_two_mk_eq_residue_lift line 499
  33. def OAI.QuadraticGaussRay.fixedGValue line 510
  34. theorem OAI.QuadraticGaussRay.residue_eq_of_four_dvd_sub line 514
  35. theorem OAI.QuadraticGaussRay.residue_eq_of_quotient_four_eq line 528
  36. def OAI.QuadraticGaussRay.residueQuotientFour line 533
  37. theorem OAI.QuadraticGaussRay.residueQuotientFour_mk line 536
  38. def OAI.QuadraticGaussRay.fixedGQuotientValue line 539
  39. theorem OAI.QuadraticGaussRay.canonicalProductG_eq_fixedGValue line 542
  40. theorem OAI.QuadraticGaussRay.canonicalProductG_eq_of_residue_eq line 557
  41. theorem OAI.QuadraticGaussRay.canonicalProductG_eq_fixed_quotient line 574