OAI/NumberTheory/Catalan/Estimates/FixedCompactReversedU16To23.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedReversedUData_16 line 11
  2. def OAI.InternalCatalan.fixedReversedUCoeff_16 line 22
  3. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_16 line 33
  4. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_16 line 45
  5. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_16 line 49
  6. def OAI.InternalCatalan.fixedReversedUData_17 line 53
  7. def OAI.InternalCatalan.fixedReversedUCoeff_17 line 64
  8. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_17 line 75
  9. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_17 line 87
  10. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_17 line 91
  11. def OAI.InternalCatalan.fixedReversedUData_18 line 95
  12. def OAI.InternalCatalan.fixedReversedUCoeff_18 line 107
  13. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_18 line 119
  14. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_18 line 132
  15. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_18 line 136
  16. def OAI.InternalCatalan.fixedReversedUData_19 line 140
  17. def OAI.InternalCatalan.fixedReversedUCoeff_19 line 152
  18. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_19 line 164
  19. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_19 line 177
  20. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_19 line 181
  21. def OAI.InternalCatalan.fixedReversedUData_20 line 185
  22. def OAI.InternalCatalan.fixedReversedUCoeff_20 line 198
  23. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_20 line 211
  24. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_20 line 225
  25. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_20 line 229
  26. def OAI.InternalCatalan.fixedReversedUData_21 line 233
  27. def OAI.InternalCatalan.fixedReversedUCoeff_21 line 246
  28. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_21 line 259
  29. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_21 line 273
  30. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_21 line 277
  31. def OAI.InternalCatalan.fixedReversedUData_22 line 281
  32. def OAI.InternalCatalan.fixedReversedUCoeff_22 line 295
  33. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_22 line 309
  34. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_22 line 324
  35. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_22 line 328
  36. def OAI.InternalCatalan.fixedReversedUData_23 line 332
  37. def OAI.InternalCatalan.fixedReversedUCoeff_23 line 346
  38. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_23 line 360
  39. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_23 line 375
  40. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_23 line 379