OAI/NumberTheory/Catalan/Polynomial/PalindromicPolynomialFrobenius.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.palindromicRat_coefficient_frobenius line 16
2. theorem OAI.InternalCatalan.palindromicRat_polynomial_eval₂_pow line 22
3. theorem OAI.InternalCatalan.palindromicRat_polynomial_T_frobenius line 33
4. theorem OAI.InternalCatalan.palindromicRat_polynomial_comp_X_pow_eval₂ line 39
5. theorem OAI.InternalCatalan.palindromicRat_polynomial_comp_X_pow_at_T line 46
6. theorem OAI.InternalCatalan.palindromicRat_int_map_eval₂ line 53
7. theorem OAI.InternalCatalan.palindromicRat_rowP_map_eval₂ line 64
8. theorem OAI.InternalCatalan.palindromicRat_rowD_map_eval₂ line 71
9. theorem OAI.InternalCatalan.palindromicRat_int_polynomial_T_frobenius line 78
10. theorem OAI.InternalCatalan.palindromicRat_PResidueSum_eval₂ line 86
11. theorem OAI.InternalCatalan.palindromicRat_DResidueSum_eval₂ line 103