OAI/NumberTheory/Catalan/FiniteMatrices/FixedGaussianPlusStep0.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedGaussianPlusState0 line 10
  2. def OAI.InternalCatalan.fixedGaussianPlusState1Row0 line 13
  3. def OAI.InternalCatalan.fixedGaussianPlusState1Row1 line 65
  4. def OAI.InternalCatalan.fixedGaussianPlusState1Row2 line 117
  5. def OAI.InternalCatalan.fixedGaussianPlusState1Row3 line 169
  6. def OAI.InternalCatalan.fixedGaussianPlusState1Row4 line 221
  7. def OAI.InternalCatalan.fixedGaussianPlusState1Row5 line 273
  8. def OAI.InternalCatalan.fixedGaussianPlusState1Row6 line 325
  9. def OAI.InternalCatalan.fixedGaussianPlusState1Row7 line 377
  10. def OAI.InternalCatalan.fixedGaussianPlusState1Row8 line 429
  11. def OAI.InternalCatalan.fixedGaussianPlusState1Row9 line 481
  12. def OAI.InternalCatalan.fixedGaussianPlusState1Row10 line 533
  13. def OAI.InternalCatalan.fixedGaussianPlusState1Row11 line 585
  14. def OAI.InternalCatalan.fixedGaussianPlusState1Row12 line 637
  15. def OAI.InternalCatalan.fixedGaussianPlusState1Row13 line 689
  16. def OAI.InternalCatalan.fixedGaussianPlusState1Row14 line 741
  17. def OAI.InternalCatalan.fixedGaussianPlusState1Row15 line 793
  18. def OAI.InternalCatalan.fixedGaussianPlusState1Row16 line 845
  19. def OAI.InternalCatalan.fixedGaussianPlusState1Row17 line 897
  20. def OAI.InternalCatalan.fixedGaussianPlusState1Row18 line 949
  21. def OAI.InternalCatalan.fixedGaussianPlusState1Row19 line 1001
  22. def OAI.InternalCatalan.fixedGaussianPlusState1Row20 line 1053
  23. def OAI.InternalCatalan.fixedGaussianPlusState1Row21 line 1105
  24. def OAI.InternalCatalan.fixedGaussianPlusState1Row22 line 1157
  25. def OAI.InternalCatalan.fixedGaussianPlusState1Row23 line 1209
  26. def OAI.InternalCatalan.fixedGaussianPlusState1Row24 line 1261
  27. def OAI.InternalCatalan.fixedGaussianPlusState1Row25 line 1313
  28. def OAI.InternalCatalan.fixedGaussianPlusState1Row26 line 1365
  29. def OAI.InternalCatalan.fixedGaussianPlusState1Row27 line 1417
  30. def OAI.InternalCatalan.fixedGaussianPlusState1Row28 line 1469
  31. def OAI.InternalCatalan.fixedGaussianPlusState1Row29 line 1521
  32. def OAI.InternalCatalan.fixedGaussianPlusState1Row30 line 1573
  33. def OAI.InternalCatalan.fixedGaussianPlusState1Row31 line 1625
  34. def OAI.InternalCatalan.fixedGaussianPlusState1Row32 line 1677
  35. def OAI.InternalCatalan.fixedGaussianPlusState1Row33 line 1729
  36. def OAI.InternalCatalan.fixedGaussianPlusState1Row34 line 1781
  37. def OAI.InternalCatalan.fixedGaussianPlusState1Row35 line 1833
  38. def OAI.InternalCatalan.fixedGaussianPlusState1Row36 line 1885
  39. def OAI.InternalCatalan.fixedGaussianPlusState1Row37 line 1937
  40. def OAI.InternalCatalan.fixedGaussianPlusState1Row38 line 1989
  41. def OAI.InternalCatalan.fixedGaussianPlusState1Row39 line 2041
  42. def OAI.InternalCatalan.fixedGaussianPlusState1Row40 line 2093
  43. def OAI.InternalCatalan.fixedGaussianPlusState1Row41 line 2145
  44. def OAI.InternalCatalan.fixedGaussianPlusState1Row42 line 2197
  45. def OAI.InternalCatalan.fixedGaussianPlusState1Row43 line 2249
  46. def OAI.InternalCatalan.fixedGaussianPlusState1Row44 line 2301
  47. def OAI.InternalCatalan.fixedGaussianPlusState1Row45 line 2353
  48. def OAI.InternalCatalan.fixedGaussianPlusState1Row46 line 2405
  49. def OAI.InternalCatalan.fixedGaussianPlusState1Row47 line 2457
  50. def OAI.InternalCatalan.fixedGaussianPlusState1 line 2509
  51. theorem OAI.InternalCatalan.fixedGaussianPlusState0_eq line 2561
  52. theorem OAI.InternalCatalan.fixedGaussianPlusStep0_pivot line 2565
  53. theorem OAI.InternalCatalan.fixedGaussianPlusStep0_cells line 2577
  54. theorem OAI.InternalCatalan.fixedGaussianPlusStep0_eq line 2611