OAI/NumberTheory/Catalan/Determinants/PalindromicRowFrobenius.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.chebyshev_U_sign_natAbs_eval line 12
  2. theorem OAI.InternalCatalan.rowP_eval₂_of_distance_lt line 23
  3. theorem OAI.InternalCatalan.rowD_eval₂_of_distance_lt line 35
  4. theorem OAI.InternalCatalan.palindromicRat_row_identity_of_distance_lt line 50
  5. theorem OAI.InternalCatalan.palindromicRat_row_identity line 91
  6. theorem OAI.InternalCatalan.palindromicRat_row_identity_auxiliary line 101
  7. theorem OAI.InternalCatalan.palindromic_base_distance_lt line 122
  8. theorem OAI.InternalCatalan.palindromic_block_row_lt line 127
  9. theorem OAI.InternalCatalan.palindromicRatRow_eq_actual_rows line 135
  10. theorem OAI.InternalCatalan.palindromicRat_rows_separated line 147
  11. theorem OAI.InternalCatalan.palindromic_rowP_frobenius line 214
  12. theorem OAI.InternalCatalan.palindromic_rowD_frobenius line 224