OAI/NumberTheory/Catalan/Estimates/FixedCompactReversedU8To15.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedReversedUData_8 line 11
  2. def OAI.InternalCatalan.fixedReversedUCoeff_8 line 18
  3. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_8 line 25
  4. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_8 line 33
  5. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_8 line 37
  6. def OAI.InternalCatalan.fixedReversedUData_9 line 41
  7. def OAI.InternalCatalan.fixedReversedUCoeff_9 line 48
  8. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_9 line 55
  9. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_9 line 63
  10. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_9 line 67
  11. def OAI.InternalCatalan.fixedReversedUData_10 line 71
  12. def OAI.InternalCatalan.fixedReversedUCoeff_10 line 79
  13. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_10 line 87
  14. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_10 line 96
  15. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_10 line 100
  16. def OAI.InternalCatalan.fixedReversedUData_11 line 104
  17. def OAI.InternalCatalan.fixedReversedUCoeff_11 line 112
  18. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_11 line 120
  19. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_11 line 129
  20. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_11 line 133
  21. def OAI.InternalCatalan.fixedReversedUData_12 line 137
  22. def OAI.InternalCatalan.fixedReversedUCoeff_12 line 146
  23. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_12 line 155
  24. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_12 line 165
  25. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_12 line 169
  26. def OAI.InternalCatalan.fixedReversedUData_13 line 173
  27. def OAI.InternalCatalan.fixedReversedUCoeff_13 line 182
  28. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_13 line 191
  29. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_13 line 201
  30. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_13 line 205
  31. def OAI.InternalCatalan.fixedReversedUData_14 line 209
  32. def OAI.InternalCatalan.fixedReversedUCoeff_14 line 219
  33. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_14 line 229
  34. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_14 line 240
  35. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_14 line 244
  36. def OAI.InternalCatalan.fixedReversedUData_15 line 248
  37. def OAI.InternalCatalan.fixedReversedUCoeff_15 line 258
  38. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_15 line 268
  39. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_15 line 279
  40. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_15 line 283