OAI/NumberTheory/Catalan/Estimates/FixedCompactReversedT40To44.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedReversedTData_40 line 10
  2. def OAI.InternalCatalan.fixedReversedTCoeff_40 line 33
  3. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_40 line 56
  4. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_40 line 80
  5. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_40 line 84
  6. def OAI.InternalCatalan.fixedReversedTData_41 line 88
  7. def OAI.InternalCatalan.fixedReversedTCoeff_41 line 111
  8. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_41 line 134
  9. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_41 line 158
  10. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_41 line 162
  11. def OAI.InternalCatalan.fixedReversedTData_42 line 166
  12. def OAI.InternalCatalan.fixedReversedTCoeff_42 line 190
  13. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_42 line 214
  14. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_42 line 239
  15. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_42 line 243
  16. def OAI.InternalCatalan.fixedReversedTData_43 line 247
  17. def OAI.InternalCatalan.fixedReversedTCoeff_43 line 271
  18. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_43 line 295
  19. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_43 line 320
  20. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_43 line 324
  21. def OAI.InternalCatalan.fixedReversedTData_44 line 328
  22. def OAI.InternalCatalan.fixedReversedTCoeff_44 line 353
  23. theorem OAI.InternalCatalan.fixed_reversedT_typed_data_44 line 378
  24. theorem OAI.InternalCatalan.fixed_reversedT_typed_coeff_44 line 404
  25. theorem OAI.InternalCatalan.fixed_reversedT_typed_tail_44 line 408