OAI/NumberTheory/Catalan/FiniteMatrices/FixedModularPlusProductRows40To41.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedLiteralModPlusRow_36 line 11
  2. def OAI.InternalCatalan.fixedLiteralModPlusRow_37 line 63
  3. def OAI.InternalCatalan.fixedLiteralModPlusRow_38 line 115
  4. def OAI.InternalCatalan.fixedLiteralModPlusRow_39 line 167
  5. def OAI.InternalCatalan.fixedLiteralModPlusRow_40 line 219
  6. def OAI.InternalCatalan.fixedLiteralModPlusRow_41 line 271
  7. def OAI.InternalCatalan.fixedLiteralModPlusRow_42 line 323
  8. def OAI.InternalCatalan.fixedLiteralModPlusRow_43 line 375
  9. def OAI.InternalCatalan.fixedLiteralModPlusRow_44 line 427
  10. def OAI.InternalCatalan.fixedLiteralModPlusRow_45 line 479
  11. def OAI.InternalCatalan.fixedLiteralModPlusRow_46 line 531
  12. def OAI.InternalCatalan.fixedLiteralModPlusRow_47 line 583
  13. def OAI.InternalCatalan.fixedLiteralModPlus line 643
  14. def OAI.InternalCatalan.fixedLiteralInvPlus line 695
  15. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_0 line 755
  16. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_1 line 760
  17. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_10 line 773
  18. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_11 line 778
  19. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_12 line 791
  20. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_13 line 796
  21. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_14 line 809
  22. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_15 line 814
  23. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_16 line 827
  24. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_17 line 832
  25. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_18 line 845
  26. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_19 line 850
  27. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_20 line 863
  28. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_21 line 868
  29. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_22 line 881
  30. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_23 line 886
  31. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_24 line 899
  32. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_25 line 904
  33. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_26 line 917
  34. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_27 line 922
  35. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_28 line 935
  36. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_29 line 940
  37. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_2 line 953
  38. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_3 line 958
  39. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_30 line 971
  40. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_31 line 976
  41. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_32 line 989
  42. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_33 line 994
  43. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_34 line 1007
  44. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_35 line 1012
  45. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_36 line 1025
  46. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_37 line 1030
  47. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_38 line 1043
  48. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_39 line 1048
  49. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_40 line 1061
  50. theorem OAI.InternalCatalan.fixedLiteralModPlus_rightInverse_row_41 line 1066