OAI/NumberTheory/DirichletL/QuadraticSieve/CrossSeparation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MixedCrossSeparation.O line 74
  2. theorem OAI.MixedCrossSeparation.ordered_cross_partition line 77
  3. def OAI.MixedCrossSeparation.crossSymbol line 137
  4. theorem OAI.MixedCrossSeparation.mixed_cross_eq_quadratic line 142
  5. def OAI.MixedCrossSeparation.convertedColumnBlock line 156
  6. def OAI.MixedCrossSeparation.quadraticCrossPhase line 162
  7. theorem OAI.MixedCrossSeparation.mixed_converted_gauss_separation line 167
  8. theorem OAI.MixedCrossSeparation.quadraticCrossPhase_sq line 226
  9. theorem OAI.MixedCrossSeparation.quadraticCrossPhase_eq_one_or_neg_one line 249
  10. theorem OAI.MixedCrossSeparation.activeConvertedGauss_separated line 257
  11. theorem OAI.MixedCrossSeparation.active_dual_row_factorization line 282
  12. theorem OAI.MixedCrossSeparation.prod_subtype_erase line 300
  13. theorem OAI.MixedCrossSeparation.restricted_prime_coprime line 317
  14. def OAI.MixedCrossSeparation.quadraticBlock line 324
  15. theorem OAI.MixedCrossSeparation.quadraticBlock_eq_productGauss line 330
  16. theorem OAI.MixedCrossSeparation.quadraticBlock_eq_rayValue line 351
  17. theorem OAI.MixedCrossSeparation.quadraticBlock_union line 363
  18. theorem OAI.MixedCrossSeparation.norm_quadraticBlock line 414
  19. def OAI.MixedCrossSeparation.quadraticRayPair line 426
  20. theorem OAI.MixedCrossSeparation.quadraticCrossPhase_eq_rayPair line 430
  21. theorem OAI.MixedCrossSeparation.mixed_converted_gauss_separation_mod_four line 461
  22. abbrev OAI.CoprimeMobiusExtension.O line 492
  23. theorem OAI.CoprimeMobiusExtension.sum_subset_sign line 494
  24. theorem OAI.CoprimeMobiusExtension.disjoint_indicator_expansion line 502
  25. theorem OAI.CoprimeMobiusExtension.double_sum_disjoint_expansion line 528
  26. theorem OAI.CoprimeMobiusExtension.sum_supersets line 565
  27. theorem OAI.CoprimeMobiusExtension.double_sum_disjoint_reindexed line 589
  28. theorem OAI.CoprimeMobiusExtension.ideal_mobius_coprime_reindex line 613