OAI/NumberTheory/Catalan/Estimates/FixedCompactReversedT24To31.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedReversedTData_24 line 11
  2. def OAI.InternalCatalan.fixedReversedTCoeff_24 line 26
  3. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_24 line 41
  4. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_24 line 57
  5. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_24 line 61
  6. def OAI.InternalCatalan.fixedReversedTData_25 line 65
  7. def OAI.InternalCatalan.fixedReversedTCoeff_25 line 80
  8. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_25 line 95
  9. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_25 line 111
  10. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_25 line 115
  11. def OAI.InternalCatalan.fixedReversedTData_26 line 119
  12. def OAI.InternalCatalan.fixedReversedTCoeff_26 line 135
  13. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_26 line 151
  14. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_26 line 168
  15. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_26 line 172
  16. def OAI.InternalCatalan.fixedReversedTData_27 line 176
  17. def OAI.InternalCatalan.fixedReversedTCoeff_27 line 192
  18. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_27 line 208
  19. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_27 line 225
  20. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_27 line 229
  21. def OAI.InternalCatalan.fixedReversedTData_28 line 233
  22. def OAI.InternalCatalan.fixedReversedTCoeff_28 line 250
  23. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_28 line 267
  24. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_28 line 285
  25. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_28 line 289
  26. def OAI.InternalCatalan.fixedReversedTData_29 line 293
  27. def OAI.InternalCatalan.fixedReversedTCoeff_29 line 310
  28. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_29 line 327
  29. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_29 line 345
  30. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_29 line 349
  31. def OAI.InternalCatalan.fixedReversedTData_30 line 353
  32. def OAI.InternalCatalan.fixedReversedTCoeff_30 line 371
  33. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_30 line 389
  34. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_30 line 408
  35. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_30 line 412
  36. def OAI.InternalCatalan.fixedReversedTData_31 line 416
  37. def OAI.InternalCatalan.fixedReversedTCoeff_31 line 434
  38. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_31 line 452
  39. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_31 line 471
  40. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_31 line 475