OAI/NumberTheory/Catalan/Estimates/FixedCompactReversedT16To23.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedReversedTData_16 line 11
  2. def OAI.InternalCatalan.fixedReversedTCoeff_16 line 22
  3. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_16 line 33
  4. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_16 line 45
  5. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_16 line 49
  6. def OAI.InternalCatalan.fixedReversedTData_17 line 53
  7. def OAI.InternalCatalan.fixedReversedTCoeff_17 line 64
  8. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_17 line 75
  9. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_17 line 87
  10. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_17 line 91
  11. def OAI.InternalCatalan.fixedReversedTData_18 line 95
  12. def OAI.InternalCatalan.fixedReversedTCoeff_18 line 107
  13. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_18 line 119
  14. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_18 line 132
  15. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_18 line 136
  16. def OAI.InternalCatalan.fixedReversedTData_19 line 140
  17. def OAI.InternalCatalan.fixedReversedTCoeff_19 line 152
  18. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_19 line 164
  19. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_19 line 177
  20. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_19 line 181
  21. def OAI.InternalCatalan.fixedReversedTData_20 line 185
  22. def OAI.InternalCatalan.fixedReversedTCoeff_20 line 198
  23. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_20 line 211
  24. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_20 line 225
  25. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_20 line 229
  26. def OAI.InternalCatalan.fixedReversedTData_21 line 233
  27. def OAI.InternalCatalan.fixedReversedTCoeff_21 line 246
  28. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_21 line 259
  29. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_21 line 273
  30. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_21 line 277
  31. def OAI.InternalCatalan.fixedReversedTData_22 line 281
  32. def OAI.InternalCatalan.fixedReversedTCoeff_22 line 295
  33. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_22 line 309
  34. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_22 line 324
  35. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_22 line 328
  36. def OAI.InternalCatalan.fixedReversedTData_23 line 332
  37. def OAI.InternalCatalan.fixedReversedTCoeff_23 line 346
  38. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_23 line 360
  39. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_23 line 375
  40. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_23 line 379