OAI/NumberTheory/Catalan/Arithmetic/OddPrimeEvenStartingZero.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.rational_residue_mul line 9
  2. theorem OAI.InternalCatalan.rational_residue_inv line 29
  3. theorem OAI.InternalCatalan.rational_residue_nat_mul_eq line 45
  4. theorem OAI.InternalCatalan.rational_residue_add line 65
  5. theorem OAI.InternalCatalan.rational_residue_sum line 85
  6. theorem OAI.InternalCatalan.scaled_two_div_den_ne_zero line 112
  7. theorem OAI.InternalCatalan.parityBoundarySum_scaled_den_ne_zero line 124
  8. theorem OAI.InternalCatalan.boundaryPlusWeight_even_scaled_den_ne_zero line 137
  9. theorem OAI.InternalCatalan.boundaryPlusWeight_odd_scaled_den_ne_zero line 154
  10. theorem OAI.InternalCatalan.boundaryMinusWeight_even_scaled_den_ne_zero line 172
  11. theorem OAI.InternalCatalan.boundaryMinusWeight_odd_scaled_den_ne_zero line 184
  12. theorem OAI.InternalCatalan.boundaryPlus_prime_sq_scaled_den_ne_zero line 194
  13. theorem OAI.InternalCatalan.boundaryMinus_prime_sq_scaled_den_ne_zero line 226
  14. def OAI.InternalCatalan.oddHarmonicRat line 267
  15. theorem OAI.InternalCatalan.oddHarmonicRat_zero line 270
  16. theorem OAI.InternalCatalan.oddHarmonicRat_succ line 273
  17. theorem OAI.InternalCatalan.oddHarmonicTerm_den_ne_zero line 279
  18. theorem OAI.InternalCatalan.oddHarmonicRat_small_den_ne_zero line 294
  19. theorem OAI.InternalCatalan.oddHarmonicTerm_scaled_zero line 306
  20. theorem OAI.InternalCatalan.oddHarmonicTerm_scaled_multiple line 317
  21. theorem OAI.InternalCatalan.oddHarmonicRat_prime_digit_reduction line 345
  22. theorem OAI.InternalCatalan.rational_residue_sub line 404
  23. theorem OAI.InternalCatalan.oddPrime_four_half_pow line 423
  24. theorem OAI.InternalCatalan.centralCoeff_residue_square_block line 440
  25. theorem OAI.InternalCatalan.centralCoeff_square_block_reduction line 472
  26. theorem OAI.InternalCatalan.boundaryMinusWeight_even_no_carry_reduction line 498
  27. theorem OAI.InternalCatalan.boundaryMinus_even_scaled_residue_sum line 519
  28. theorem OAI.InternalCatalan.boundaryMinus_even_odd_remainder_zero line 569