OAI/NumberTheory/DirichletL/RowCompletion/FreePrimePools.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalRowCompletion.freePrimePool line 85
  2. lemma OAI.CanonicalRowCompletion.mem_freePrimePool line 88
  3. lemma OAI.CanonicalRowCompletion.residual_nonresidual_disjoint line 92
  4. theorem OAI.CanonicalRowCompletion.freePrimePool_eq_residual_union line 99
  5. def OAI.CanonicalRowCompletion.primeUnionToFree line 145
  6. lemma OAI.CanonicalRowCompletion.primeUnionToFree_val line 156
  7. lemma OAI.CanonicalRowCompletion.primeUnionToFree_bijective line 160
  8. def OAI.CanonicalRowCompletion.primeUnionEquiv line 187
  9. lemma OAI.CanonicalRowCompletion.primeUnionEquiv_val line 193
  10. theorem OAI.CanonicalRowCompletion.prod_freePrimeIndex_eq line 198
  11. theorem OAI.CanonicalRowCompletion.goodMaskFreePrimePool line 225
  12. def OAI.CanonicalRowCompletion.goodMaskFreePrimeEquiv line 234
  13. lemma OAI.CanonicalRowCompletion.goodMaskFreePrimeEquiv_val line 241
  14. lemma OAI.CanonicalRowCompletion.goodMaskFreePrimeEquiv_residual_exponent line 246
  15. lemma OAI.CanonicalRowCompletion.goodMaskFreePrimeEquiv_nonresidual_exponent line 257
  16. theorem OAI.CanonicalRowCompletion.goodMaskFreePrimeEquiv_exponent line 268
  17. def OAI.CanonicalRowCompletion.optionalPrimeActive line 287
  18. lemma OAI.CanonicalRowCompletion.mem_optionalPrimeActive line 291
  19. def OAI.CanonicalRowCompletion.activePrimeUnionMap line 295
  20. lemma OAI.CanonicalRowCompletion.activePrimeUnionMap_bijective line 301
  21. def OAI.CanonicalRowCompletion.activePrimeUnionEquiv line 321
  22. lemma OAI.CanonicalRowCompletion.activePrimeUnionEquiv_inl line 326
  23. lemma OAI.CanonicalRowCompletion.activePrimeUnionEquiv_inr line 331
  24. theorem OAI.CanonicalRowCompletion.prod_activePrimeUnionEquiv line 336
  25. theorem OAI.CanonicalRowCompletion.sum_activePrimeUnionEquiv line 347
  26. theorem OAI.CanonicalRowCompletion.sum_prime_active_sets line 357
  27. def OAI.CanonicalRowCompletion.nonresidualPoolEquiv line 368
  28. lemma OAI.CanonicalRowCompletion.nonresidualPoolEquiv_val line 379
  29. lemma OAI.CanonicalRowCompletion.nonresidualPoolEquiv_exponent line 384
  30. def OAI.CanonicalRowCompletion.goodMaskFreePrimeFiberEquiv line 404
  31. lemma OAI.CanonicalRowCompletion.goodMaskFreePrimeFiberEquiv_val line 412
  32. theorem OAI.CanonicalRowCompletion.goodMaskFreePrimeFiberEquiv_exponent line 418
  33. def OAI.CanonicalRowCompletion.goodMaskActivePrimeEquiv line 456
  34. lemma OAI.CanonicalRowCompletion.goodMaskActivePrimeEquiv_residual_val line 462
  35. lemma OAI.CanonicalRowCompletion.goodMaskActivePrimeEquiv_nonresidual_val line 469
  36. theorem OAI.CanonicalRowCompletion.goodMaskActivePrimeEquiv_exponent line 476
  37. lemma OAI.CanonicalRowCompletion.reflection_row_mask_bad line 494
  38. lemma OAI.CanonicalRowCompletion.residual_coprime_free_base line 499
  39. def OAI.CompletedGauss.residualZeroLabel line 515
  40. theorem OAI.CompletedGauss.sum_labels_drop_residual line 517
  41. lemma OAI.CompletedGauss.reflectedBranch_residual_label_zero line 536
  42. lemma OAI.CompletedGauss.reflectionExtractedDivisor_drop_residual line 546
  43. lemma OAI.CompletedGauss.reflectedBranch_drop_residual line 558
  44. def OAI.CompletedGauss.residualLabelVia line 585
  45. lemma OAI.CompletedGauss.residualLabelVia_apply line 589
  46. theorem OAI.CompletedGauss.sum_labels_drop_residual_equiv line 593
  47. lemma OAI.CompletedGauss.reflectedBranch_residual_zero_equiv line 606
  48. lemma OAI.CompletedGauss.reflectionExtractedDivisor_drop_residual_equiv line 616
  49. lemma OAI.CompletedGauss.reflectedBranch_drop_residual_equiv line 630