OAI/NumberTheory/Catalan/FiniteMatrices/FixedLiteralBaseRelationsRows0To1.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedLiteralModZeroRow_36 line 13
  2. def OAI.InternalCatalan.fixedLiteralModZeroRow_37 line 65
  3. def OAI.InternalCatalan.fixedLiteralModZeroRow_38 line 117
  4. def OAI.InternalCatalan.fixedLiteralModZeroRow_39 line 169
  5. def OAI.InternalCatalan.fixedLiteralModZeroRow_40 line 221
  6. def OAI.InternalCatalan.fixedLiteralModZeroRow_41 line 273
  7. def OAI.InternalCatalan.fixedLiteralModZeroRow_42 line 325
  8. def OAI.InternalCatalan.fixedLiteralModZeroRow_43 line 377
  9. def OAI.InternalCatalan.fixedLiteralModZeroRow_44 line 429
  10. def OAI.InternalCatalan.fixedLiteralModZeroRow_45 line 481
  11. def OAI.InternalCatalan.fixedLiteralModZeroRow_46 line 533
  12. def OAI.InternalCatalan.fixedLiteralModZeroRow_47 line 585
  13. def OAI.InternalCatalan.fixedLiteralModZero line 645
  14. def OAI.InternalCatalan.fixedLiteralInvZero line 697
  15. def OAI.InternalCatalan.fixedLiteralBaseMod line 757
  16. theorem OAI.InternalCatalan.fixedLiteralBaseMod_zero line 809
  17. theorem OAI.InternalCatalan.fixedLiteralBaseMod_auxiliary line 813
  18. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_0 line 825
  19. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_1 line 830
  20. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_10 line 843
  21. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_11 line 848
  22. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_12 line 861
  23. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_13 line 866
  24. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_14 line 879
  25. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_15 line 884
  26. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_16 line 897
  27. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_17 line 902
  28. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_18 line 915
  29. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_19 line 920
  30. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_20 line 933
  31. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_21 line 938
  32. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_22 line 951
  33. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_23 line 956
  34. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_24 line 969
  35. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_25 line 974
  36. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_26 line 987
  37. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_27 line 992
  38. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_28 line 1005
  39. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_29 line 1010
  40. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_2 line 1023
  41. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_3 line 1028
  42. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_30 line 1041
  43. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_31 line 1046
  44. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_32 line 1059
  45. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_33 line 1064
  46. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_34 line 1077
  47. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_35 line 1082
  48. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_36 line 1095
  49. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_37 line 1100
  50. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_38 line 1113
  51. theorem OAI.InternalCatalan.fixedLiteralModZero_rightInverse_row_39 line 1118
  52. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_0 line 1131
  53. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_0 line 1136
  54. theorem OAI.InternalCatalan.fixedLiteralBaseMod_plus_row_1 line 1141
  55. theorem OAI.InternalCatalan.fixedLiteralBaseMod_minus_row_1 line 1146