OAI/NumberTheory/DirichletL/CubicSieve/CubeLabels.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FirstPassCubeLabels.cross_sixth line 78
  2. theorem OAI.FirstPassCubeLabels.reverse_cross_eq_quadratic line 93
  3. theorem OAI.FirstPassCubeLabels.local_quadratic_sq line 110
  4. theorem OAI.FirstPassCubeLabels.crt_exponent_table line 119
  5. theorem OAI.FirstPassCubeLabels.active_cube_cross_local line 126
  6. def OAI.FirstPassCubeLabels.cubeOddSupport line 165
  7. def OAI.FirstPassCubeLabels.mixedCubeCross line 168
  8. theorem OAI.FirstPassCubeLabels.mixedCubeCross_eq_ordered line 176
  9. theorem OAI.FirstPassCubeLabels.cube_cross_local_if line 188
  10. theorem OAI.FirstPassCubeLabels.mixedCubeCross_eq_row_quadratic line 211
  11. theorem OAI.FirstPassCubeLabels.mixedCubeCross_eq_ray_expansion line 248
  12. abbrev OAI.QuadraticSquarefreeKernel.O line 272
  13. def OAI.QuadraticSquarefreeKernel.squarePart line 274
  14. def OAI.QuadraticSquarefreeKernel.squarefreePart line 276
  15. theorem OAI.QuadraticSquarefreeKernel.squarePart_sq_mul_squarefreePart line 279
  16. theorem OAI.QuadraticSquarefreeKernel.squarefree_squarefreePart line 283
  17. theorem OAI.QuadraticSquarefreeKernel.squarePart_ne_zero line 286
  18. theorem OAI.QuadraticSquarefreeKernel.squarefree_decomposition_unique line 292
  19. theorem OAI.QuadraticSquarefreeKernel.squarePart_mul_squarefree line 317
  20. def OAI.QuadraticSquarefreeKernel.decompositionEquiv line 323
  21. theorem OAI.QuadraticSquarefreeKernel.squarefree_decomposition_tsum line 334
  22. theorem OAI.QuadraticSquarefreeKernel.norm_decomposition line 341
  23. theorem OAI.QuadraticSquarefreeKernel.quadraticRow_mul line 347
  24. theorem OAI.QuadraticSquarefreeKernel.quadraticRow_square line 353
  25. theorem OAI.QuadraticSquarefreeKernel.quadraticRow_primary_decomposition line 361
  26. theorem OAI.QuadraticSquarefreeKernel.quadraticRow_primary_tsum_decomposition line 373
  27. abbrev OAI.QuadraticMainBoundary.O line 397
  28. def OAI.QuadraticMainBoundary.cutoffDifference line 400
  29. theorem OAI.QuadraticMainBoundary.norm_pos line 404
  30. theorem OAI.QuadraticMainBoundary.norm_one_le line 408
  31. theorem OAI.QuadraticMainBoundary.norm_le_of_dvd line 412
  32. theorem OAI.QuadraticMainBoundary.cutoffDifference_nonzero_iff line 418
  33. theorem OAI.QuadraticMainBoundary.cutoffDifference_eq_neg_one_of_nonzero line 427
  34. theorem OAI.QuadraticMainBoundary.squarePart_dvd line 433
  35. theorem OAI.QuadraticMainBoundary.cutoffDifference_eq_zero_of_product_le line 456
  36. theorem OAI.QuadraticMainBoundary.main_boundary_localization line 466
  37. theorem OAI.QuadraticMainBoundary.cutoffDifference_of_common_one line 512
  38. abbrev OAI.QuadraticDivisorCancellation.O line 521
  39. def OAI.QuadraticDivisorCancellation.normalizedRow line 524
  40. theorem OAI.QuadraticDivisorCancellation.normalizedRow_mul line 528
  41. theorem OAI.QuadraticDivisorCancellation.normalizedRow_one line 534
  42. def OAI.QuadraticDivisorCancellation.normalizedRowHom line 538
  43. theorem OAI.QuadraticDivisorCancellation.normalizedRow_prod line 544
  44. theorem OAI.QuadraticDivisorCancellation.normalizedRow_sq line 549
  45. theorem OAI.QuadraticDivisorCancellation.double_divisor_factorization line 559
  46. theorem OAI.QuadraticDivisorCancellation.actual_double_divisor_cancellation line 590
  47. theorem OAI.QuadraticDivisorCancellation.actual_double_divisor_cancellation_coprime line 610