OAI/NumberTheory/Catalan/Polynomial/PalindromicCoefficientMatrices.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InternalCatalan.palindromicU line 19
2. def OAI.InternalCatalan.palindromicQ line 22
3. theorem OAI.InternalCatalan.palindromicU_factor line 25
4. theorem OAI.InternalCatalan.palindromicU_coeff_below line 30
5. theorem OAI.InternalCatalan.palindromicU_coeff_self line 34
6. theorem OAI.InternalCatalan.palindromicQ_coeff_below line 45
7. theorem OAI.InternalCatalan.palindromicQ_coeff_self line 49
8. def OAI.InternalCatalan.palindromicUCoeffMatrix line 73
9. def OAI.InternalCatalan.palindromicQCoeffMatrix line 76
10. theorem OAI.InternalCatalan.palindromicUCoeffMatrix_lower line 79
11. theorem OAI.InternalCatalan.palindromicQCoeffMatrix_lower line 84
12. theorem OAI.InternalCatalan.det_palindromicUCoeffMatrix line 89
13. theorem OAI.InternalCatalan.det_palindromicQCoeffMatrix line 94
14. theorem OAI.InternalCatalan.palindromic_two_ne_zero line 102
15. theorem OAI.InternalCatalan.det_palindromicUCoeffMatrix_ne_zero line 112
16. theorem OAI.InternalCatalan.det_palindromicQCoeffMatrix_ne_zero line 119