OAI/NumberTheory/Catalan/Estimates/FixedCompactReversedU32To39.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedReversedUData_32 line 11
  2. def OAI.InternalCatalan.fixedReversedUCoeff_32 line 30
  3. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_32 line 49
  4. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_32 line 69
  5. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_32 line 73
  6. def OAI.InternalCatalan.fixedReversedUData_33 line 77
  7. def OAI.InternalCatalan.fixedReversedUCoeff_33 line 96
  8. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_33 line 115
  9. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_33 line 135
  10. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_33 line 139
  11. def OAI.InternalCatalan.fixedReversedUData_34 line 143
  12. def OAI.InternalCatalan.fixedReversedUCoeff_34 line 163
  13. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_34 line 183
  14. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_34 line 204
  15. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_34 line 208
  16. def OAI.InternalCatalan.fixedReversedUData_35 line 212
  17. def OAI.InternalCatalan.fixedReversedUCoeff_35 line 232
  18. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_35 line 252
  19. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_35 line 273
  20. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_35 line 277
  21. def OAI.InternalCatalan.fixedReversedUData_36 line 281
  22. def OAI.InternalCatalan.fixedReversedUCoeff_36 line 302
  23. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_36 line 323
  24. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_36 line 345
  25. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_36 line 349
  26. def OAI.InternalCatalan.fixedReversedUData_37 line 353
  27. def OAI.InternalCatalan.fixedReversedUCoeff_37 line 374
  28. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_37 line 395
  29. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_37 line 417
  30. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_37 line 421
  31. def OAI.InternalCatalan.fixedReversedUData_38 line 425
  32. def OAI.InternalCatalan.fixedReversedUCoeff_38 line 447
  33. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_38 line 469
  34. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_38 line 492
  35. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_38 line 496
  36. def OAI.InternalCatalan.fixedReversedUData_39 line 500
  37. def OAI.InternalCatalan.fixedReversedUCoeff_39 line 522
  38. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_39 line 544
  39. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_39 line 567
  40. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_39 line 571