OAI/NumberTheory/Catalan/Estimates/PalindromicExtractedEntries.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.palindromicZModIntCast_apply line 14
  2. theorem OAI.InternalCatalan.palindromic_actual_P_extraction line 17
  3. theorem OAI.InternalCatalan.palindromic_actual_D_extraction line 28
  4. theorem OAI.InternalCatalan.palindromic_actual_P_extraction_below line 38
  5. theorem OAI.InternalCatalan.palindromic_actual_extracted_rows line 45
  6. def OAI.InternalCatalan.palindromicBaseRawContraction line 70
  7. def OAI.InternalCatalan.palindromicExtractedRawContraction line 77
  8. theorem OAI.InternalCatalan.palindromicExtractedRawContraction_factor line 89
  9. def OAI.InternalCatalan.palindromicBaseFilterWeight line 101
  10. def OAI.InternalCatalan.palindromicBaseFilteredContraction line 104
  11. def OAI.InternalCatalan.palindromicExtractedFilteredEntry line 109
  12. theorem OAI.InternalCatalan.palindromicExtractedFilteredEntry_factor line 114
  13. theorem OAI.InternalCatalan.palindromicBaseRawContraction_eq_residue line 132
  14. theorem OAI.InternalCatalan.palindromicBaseFilteredContraction_eq_fixedBase line 139
  15. theorem OAI.InternalCatalan.palindromicBaseFilteredContraction_eq_fixedB0 line 152
  16. theorem OAI.InternalCatalan.palindromicBaseFilteredContraction_eq_fixedB1 line 158
  17. theorem OAI.InternalCatalan.palindromicExtractedFilteredEntry_eq_fixedB line 164