OAI/NumberTheory/Catalan/Arithmetic/OddPrimeCentralZetaContraction.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.centralCoeffKernel_odd_prime_den_ne_zero line 16
  2. theorem OAI.InternalCatalan.rawCatalanCoeffRat_odd_prime_den_ne_zero line 24
  3. theorem OAI.InternalCatalan.rawCatalanTerm_prime_sq_reduction line 36
  4. theorem OAI.InternalCatalan.momentUpperStrip_term_zero line 60
  5. theorem OAI.InternalCatalan.momentUpperStrip_term_multiple line 86
  6. def OAI.InternalCatalan.momentUpperPrefix line 172
  7. theorem OAI.InternalCatalan.momentUpperPrefix_zero line 176
  8. theorem OAI.InternalCatalan.momentUpperPrefix_succ line 179
  9. theorem OAI.InternalCatalan.momentUpperPrefix_of_le line 185
  10. theorem OAI.InternalCatalan.momentRat_upper_prefix line 193
  11. theorem OAI.InternalCatalan.momentUpperPrefix_prime_digit_reduction line 207
  12. def OAI.InternalCatalan.momentRatSigned line 261
  13. theorem OAI.InternalCatalan.momentRatSigned_natCast line 265
  14. theorem OAI.InternalCatalan.momentRatSigned_neg_one line 269
  15. theorem OAI.InternalCatalan.momentRatSigned_upper_prefix line 273
  16. theorem OAI.InternalCatalan.momentRat_upper_prime_digit_reduction line 286
  17. theorem OAI.InternalCatalan.momentRat_prime_digit_reduction_of_lt line 316
  18. theorem OAI.InternalCatalan.momentRat_prime_digit_reduction line 335
  19. theorem OAI.InternalCatalan.rawEntryRat_zero_prime_digit_reduction line 361
  20. theorem OAI.InternalCatalan.rawEntryRat_prime_digit_reduction line 461
  21. theorem OAI.InternalCatalan.filterCoeffRat_prime_den_ne_zero line 498
  22. theorem OAI.InternalCatalan.filteredEntryRat_prime_scaled_residue_sum line 506
  23. def OAI.InternalCatalan.oddPrimeExtractedP line 563
  24. def OAI.InternalCatalan.oddPrimeExtractedD line 566
  25. theorem OAI.InternalCatalan.rawEntryRat_general_column_layer line 569
  26. theorem OAI.InternalCatalan.palindromic_P_digit_contraction line 633
  27. theorem OAI.InternalCatalan.palindromic_D_digit_contraction line 671
  28. theorem OAI.InternalCatalan.palindromic_rawEntryRat_prime_digit_reduction line 683
  29. theorem OAI.InternalCatalan.oddPrime_central_P_coefficient line 732
  30. theorem OAI.InternalCatalan.rowD_zetaRat_central_reduction_coeff line 772
  31. theorem OAI.InternalCatalan.rowD_zetaRat_central_reduction line 850