OAI/NumberTheory/Catalan/FiniteMatrices/FixedDeterminantsNonzero.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_32 line 24
  2. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_32 line 29
  3. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_33 line 34
  4. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_33 line 39
  5. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_34 line 52
  6. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_34 line 57
  7. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_35 line 62
  8. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_35 line 67
  9. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_36 line 80
  10. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_36 line 85
  11. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_37 line 90
  12. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_37 line 95
  13. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_38 line 108
  14. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_38 line 113
  15. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_39 line 118
  16. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_39 line 123
  17. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_40 line 136
  18. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_40 line 141
  19. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_41 line 146
  20. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_41 line 151
  21. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_42 line 164
  22. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_42 line 169
  23. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_43 line 174
  24. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_43 line 179
  25. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_44 line 192
  26. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_44 line 197
  27. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_45 line 202
  28. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_45 line 207
  29. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_46 line 220
  30. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_46 line 225
  31. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_47 line 230
  32. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_47 line 235
  33. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_4 line 248
  34. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_4 line 253
  35. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_5 line 258
  36. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_5 line 263
  37. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_6 line 276
  38. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_6 line 281
  39. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_7 line 286
  40. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_7 line 291
  41. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_8 line 304
  42. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_8 line 309
  43. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_9 line 314
  44. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_9 line 319
  45. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus line 332
  46. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus line 385
  47. theorem OAI.InternalCatalan.fixedCanonicalMatrix_zero_mod line 447
  48. theorem OAI.InternalCatalan.fixedCanonicalMatrix_plus_mod line 456
  49. theorem OAI.InternalCatalan.fixedCanonicalMatrix_minus_mod line 466
  50. theorem OAI.InternalCatalan.fixedMatrix_zero_det_ne_zero line 487
  51. theorem OAI.InternalCatalan.fixedMatrix_one_det_ne_zero line 497
  52. theorem OAI.InternalCatalan.fixedMatrix_neg_one_det_ne_zero line 507