OAI/NumberTheory/Catalan/Estimates/FixedCompactReversedU0To7.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedReversedUData_0 line 11
  2. def OAI.InternalCatalan.fixedReversedUCoeff_0 line 14
  3. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_0 line 17
  4. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_0 line 21
  5. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_0 line 25
  6. def OAI.InternalCatalan.fixedReversedUData_1 line 29
  7. def OAI.InternalCatalan.fixedReversedUCoeff_1 line 32
  8. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_1 line 35
  9. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_1 line 39
  10. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_1 line 43
  11. def OAI.InternalCatalan.fixedReversedUData_2 line 47
  12. def OAI.InternalCatalan.fixedReversedUCoeff_2 line 51
  13. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_2 line 55
  14. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_2 line 60
  15. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_2 line 64
  16. def OAI.InternalCatalan.fixedReversedUData_3 line 68
  17. def OAI.InternalCatalan.fixedReversedUCoeff_3 line 72
  18. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_3 line 76
  19. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_3 line 81
  20. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_3 line 85
  21. def OAI.InternalCatalan.fixedReversedUData_4 line 89
  22. def OAI.InternalCatalan.fixedReversedUCoeff_4 line 94
  23. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_4 line 99
  24. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_4 line 105
  25. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_4 line 109
  26. def OAI.InternalCatalan.fixedReversedUData_5 line 113
  27. def OAI.InternalCatalan.fixedReversedUCoeff_5 line 118
  28. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_5 line 123
  29. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_5 line 129
  30. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_5 line 133
  31. def OAI.InternalCatalan.fixedReversedUData_6 line 137
  32. def OAI.InternalCatalan.fixedReversedUCoeff_6 line 143
  33. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_6 line 149
  34. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_6 line 156
  35. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_6 line 160
  36. def OAI.InternalCatalan.fixedReversedUData_7 line 164
  37. def OAI.InternalCatalan.fixedReversedUCoeff_7 line 170
  38. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_7 line 176
  39. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_7 line 183
  40. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_7 line 187