OAI/NumberTheory/Catalan/Arithmetic/PrimeNonvanishing.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.oddPrime_multiple_sum_gather line 19
  2. theorem OAI.InternalCatalan.palindromic_filteredEntryRat_prime_digit_reduction line 57
  3. theorem OAI.InternalCatalan.palindromicScaledRatMatrix_entry_den_ne_zero line 116
  4. theorem OAI.InternalCatalan.palindromicScaledResidueMatrix_eq_extracted line 122
  5. theorem OAI.InternalCatalan.palindromicScaledResidueMatrix_eq_blocks line 128
  6. def OAI.InternalCatalan.palindromicPrimeCutoff line 134
  7. theorem OAI.InternalCatalan.determinantRat_prime_ne_zero_of_fixed line 136
  8. theorem OAI.InternalCatalan.determinantRat_prime_eventually_ne_zero_of_fixed line 158
  9. theorem OAI.InternalCatalan.determinant_prime_eventually_ne_zero_of_fixed line 168
  10. theorem OAI.InternalCatalan.padicValRat_eq_zero_of_palindromicRatResidue_ne_zero line 192
  11. theorem OAI.InternalCatalan.palindromicScaledRatMatrix_det_valuation_zero line 209
  12. theorem OAI.InternalCatalan.determinantRat_prime_valuation_of_fixed line 236
  13. theorem OAI.InternalCatalan.determinantRat_prime_ne_zero line 264
  14. theorem OAI.InternalCatalan.determinantRat_prime_valuation line 269
  15. theorem OAI.InternalCatalan.determinant_prime_eventually_ne_zero line 275
  16. def OAI.InternalCatalan.nonzeroPrimeScale line 280
  17. theorem OAI.InternalCatalan.nonzeroPrimeScale_bound line 283
  18. theorem OAI.InternalCatalan.nonzeroPrimeScale_prime line 288
  19. theorem OAI.InternalCatalan.nonzeroPrimeScale_tendsto line 292
  20. theorem OAI.InternalCatalan.determinantRat_nonzeroPrimeScale_ne_zero line 301
  21. theorem OAI.InternalCatalan.determinant_nonzeroPrimeScale_ne_zero line 308
  22. theorem OAI.InternalCatalan.exists_nonzero_prime_scales line 313