OAI/NumberTheory/Catalan/Estimates/FixedCompactReversedU40To43.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedReversedUData_40 line 10
  2. def OAI.InternalCatalan.fixedReversedUCoeff_40 line 33
  3. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_40 line 56
  4. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_40 line 80
  5. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_40 line 84
  6. def OAI.InternalCatalan.fixedReversedUData_41 line 88
  7. def OAI.InternalCatalan.fixedReversedUCoeff_41 line 111
  8. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_41 line 134
  9. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_41 line 158
  10. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_41 line 162
  11. def OAI.InternalCatalan.fixedReversedUData_42 line 166
  12. def OAI.InternalCatalan.fixedReversedUCoeff_42 line 190
  13. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_42 line 214
  14. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_42 line 239
  15. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_42 line 243
  16. def OAI.InternalCatalan.fixedReversedUData_43 line 247
  17. def OAI.InternalCatalan.fixedReversedUCoeff_43 line 271
  18. theorem OAI.InternalCatalan.fixed_reversedU_typed_data_43 line 295
  19. theorem OAI.InternalCatalan.fixed_reversedU_typed_coeff_43 line 320
  20. theorem OAI.InternalCatalan.fixed_reversedU_typed_tail_43 line 324