OAI/NumberTheory/Catalan/Arithmetic/OddPrimeFilterDigits.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.prime_add_integral line 14
2. theorem OAI.InternalCatalan.prime_sub_integral line 21
3. theorem OAI.InternalCatalan.prime_mul_integral line 27
4. theorem OAI.InternalCatalan.prime_div_integral line 37
5. theorem OAI.InternalCatalan.prime_sum_integral line 45
6. theorem OAI.InternalCatalan.prime_nat_den_valuation line 56
7. theorem OAI.InternalCatalan.centralCoeff_odd_prime_valuation_zero_of_lt line 62
8. theorem OAI.InternalCatalan.momentScalar_even_odd_prime_valuation_zero_of_lt line 70
9. theorem OAI.InternalCatalan.momentScalar_odd_prime_valuation_nonneg line 89
10. theorem OAI.InternalCatalan.boundaryMinus_odd_prime_valuation_nonneg line 100
11. theorem OAI.InternalCatalan.boundaryPlus_odd_prime_valuation_nonneg line 124
12. theorem OAI.InternalCatalan.momentRat_odd_prime_small_valuation_nonneg line 152
13. theorem OAI.InternalCatalan.momentRat_odd_prime_small_den_ne_zero line 176
14. theorem OAI.InternalCatalan.momentRat_odd_prime_small_scaled_reduction line 182
15. theorem OAI.InternalCatalan.nat_fraction_reduced_residue line 202
16. theorem OAI.InternalCatalan.centralCoeff_reduced_residue line 230
17. theorem OAI.InternalCatalan.centralBinom_residue_digit_no_carry line 239
18. theorem OAI.InternalCatalan.centralCoeff_denominator_digit line 254
19. theorem OAI.InternalCatalan.centralCoeff_finite_digit_no_carry line 262
20. theorem OAI.InternalCatalan.centralCoeff_digit_no_carry line 270
21. theorem OAI.InternalCatalan.boundaryFactor_even_digit_reduction line 289
22. theorem OAI.InternalCatalan.boundaryFactor_even_carry_reduction line 323
23. theorem OAI.InternalCatalan.filterCoeffRat_den_one line 336
24. theorem OAI.InternalCatalan.filterCoeffRat_reduced_residue line 342
25. theorem OAI.InternalCatalan.filterBinomial_prime_digit line 352
26. theorem OAI.InternalCatalan.filterCoeffRat_prime_digit_reduction line 364