OAI/NumberTheory/Catalan/Determinants/FixedCompactRowsAll.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedRowPData_4 line 56
  2. def OAI.InternalCatalan.fixedRowPCoeff_4 line 61
  3. theorem OAI.InternalCatalan.fixed_rowP_typed_coeff_4 line 66
  4. theorem OAI.InternalCatalan.fixed_rowP_typed_tail_4 line 70
  5. theorem OAI.InternalCatalan.fixed_rowP_typed_scalar_4 line 74
  6. theorem OAI.InternalCatalan.fixed_rowP_typed_factor_4 line 78
  7. theorem OAI.InternalCatalan.fixed_rowP_typed_4 line 104
  8. def OAI.InternalCatalan.fixedRowDData_4 line 112
  9. def OAI.InternalCatalan.fixedRowDCoeff_4 line 115
  10. theorem OAI.InternalCatalan.fixed_rowD_typed_coeff_4 line 118
  11. theorem OAI.InternalCatalan.fixed_rowD_typed_tail_4 line 122
  12. theorem OAI.InternalCatalan.fixed_rowD_typed_4 line 126
  13. def OAI.InternalCatalan.fixedRowPData_19 line 142
  14. def OAI.InternalCatalan.fixedRowPCoeff_19 line 161
  15. theorem OAI.InternalCatalan.fixed_rowP_typed_coeff_19 line 180
  16. theorem OAI.InternalCatalan.fixed_rowP_typed_tail_19 line 184
  17. theorem OAI.InternalCatalan.fixed_rowP_typed_scalar_19 line 188
  18. theorem OAI.InternalCatalan.fixed_rowP_typed_factor_19 line 192
  19. theorem OAI.InternalCatalan.fixed_rowP_typed_19 line 218
  20. def OAI.InternalCatalan.fixedRowDData_19 line 226
  21. def OAI.InternalCatalan.fixedRowDCoeff_19 line 245
  22. theorem OAI.InternalCatalan.fixed_rowD_typed_coeff_19 line 264
  23. theorem OAI.InternalCatalan.fixed_rowD_typed_tail_19 line 268
  24. theorem OAI.InternalCatalan.fixed_rowD_typed_scalar_19 line 272
  25. theorem OAI.InternalCatalan.fixed_rowD_typed_factor_19 line 276
  26. theorem OAI.InternalCatalan.fixed_rowD_typed_19 line 302
  27. def OAI.InternalCatalan.fixedRowPData_20 line 324
  28. def OAI.InternalCatalan.fixedRowPCoeff_20 line 345
  29. theorem OAI.InternalCatalan.fixed_rowP_typed_coeff_20 line 366
  30. theorem OAI.InternalCatalan.fixed_rowP_typed_tail_20 line 370
  31. theorem OAI.InternalCatalan.fixed_rowP_typed_scalar_20 line 374
  32. theorem OAI.InternalCatalan.fixed_rowP_typed_factor_20 line 378
  33. theorem OAI.InternalCatalan.fixed_rowP_typed_20 line 404
  34. def OAI.InternalCatalan.fixedRowDData_20 line 412
  35. def OAI.InternalCatalan.fixedRowDCoeff_20 line 431
  36. theorem OAI.InternalCatalan.fixed_rowD_typed_coeff_20 line 450
  37. theorem OAI.InternalCatalan.fixed_rowD_typed_tail_20 line 454
  38. theorem OAI.InternalCatalan.fixed_rowD_typed_scalar_20 line 458
  39. theorem OAI.InternalCatalan.fixed_rowD_typed_factor_20 line 462
  40. theorem OAI.InternalCatalan.fixed_rowD_typed_20 line 488