OAI/NumberTheory/Catalan/FiniteMatrices/FixedDeterminantGoodPrimes.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.palindromicRatResidue_prod line 15
  2. theorem OAI.InternalCatalan.palindromicRatResidue_det line 32
  3. theorem OAI.InternalCatalan.fixedB0_det_residue line 62
  4. theorem OAI.InternalCatalan.fixedB1_det_residue line 67
  5. theorem OAI.InternalCatalan.fixedMatrix_one_det_residue line 72
  6. theorem OAI.InternalCatalan.fixedMatrix_neg_one_det_residue line 87
  7. theorem OAI.InternalCatalan.rational_det_ne_zero_of_residue_det_ne_zero line 102
  8. theorem OAI.InternalCatalan.palindromicRatResidue_ne_zero_of_bounds line 125
  9. def OAI.InternalCatalan.fixedDeterminantPrimeCutoff line 141
  10. theorem OAI.InternalCatalan.fixedDeterminantPrimeCutoff_ge_260 line 146
  11. theorem OAI.InternalCatalan.fixedDeterminants_residue_ne_zero_of_lt line 150
  12. theorem OAI.InternalCatalan.fixedDeterminants_mod_prime_ne_zero_of_lt line 163
  13. theorem OAI.InternalCatalan.fixedDeterminants_mod_prime_eventually_ne_zero line 182
  14. theorem OAI.InternalCatalan.fixedDeterminants_mod_prime_ne_zero_of_base_certificate line 194