OAI/NumberTheory/Catalan/FiniteMatrices/FixedGaussianZeroStep0.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedGaussianZeroState0 line 10
  2. def OAI.InternalCatalan.fixedGaussianZeroState1Row0 line 13
  3. def OAI.InternalCatalan.fixedGaussianZeroState1Row1 line 65
  4. def OAI.InternalCatalan.fixedGaussianZeroState1Row2 line 117
  5. def OAI.InternalCatalan.fixedGaussianZeroState1Row3 line 169
  6. def OAI.InternalCatalan.fixedGaussianZeroState1Row4 line 221
  7. def OAI.InternalCatalan.fixedGaussianZeroState1Row5 line 273
  8. def OAI.InternalCatalan.fixedGaussianZeroState1Row6 line 325
  9. def OAI.InternalCatalan.fixedGaussianZeroState1Row7 line 377
  10. def OAI.InternalCatalan.fixedGaussianZeroState1Row8 line 429
  11. def OAI.InternalCatalan.fixedGaussianZeroState1Row9 line 481
  12. def OAI.InternalCatalan.fixedGaussianZeroState1Row10 line 533
  13. def OAI.InternalCatalan.fixedGaussianZeroState1Row11 line 585
  14. def OAI.InternalCatalan.fixedGaussianZeroState1Row12 line 637
  15. def OAI.InternalCatalan.fixedGaussianZeroState1Row13 line 689
  16. def OAI.InternalCatalan.fixedGaussianZeroState1Row14 line 741
  17. def OAI.InternalCatalan.fixedGaussianZeroState1Row15 line 793
  18. def OAI.InternalCatalan.fixedGaussianZeroState1Row16 line 845
  19. def OAI.InternalCatalan.fixedGaussianZeroState1Row17 line 897
  20. def OAI.InternalCatalan.fixedGaussianZeroState1Row18 line 949
  21. def OAI.InternalCatalan.fixedGaussianZeroState1Row19 line 1001
  22. def OAI.InternalCatalan.fixedGaussianZeroState1Row20 line 1053
  23. def OAI.InternalCatalan.fixedGaussianZeroState1Row21 line 1105
  24. def OAI.InternalCatalan.fixedGaussianZeroState1Row22 line 1157
  25. def OAI.InternalCatalan.fixedGaussianZeroState1Row23 line 1209
  26. def OAI.InternalCatalan.fixedGaussianZeroState1Row24 line 1261
  27. def OAI.InternalCatalan.fixedGaussianZeroState1Row25 line 1313
  28. def OAI.InternalCatalan.fixedGaussianZeroState1Row26 line 1365
  29. def OAI.InternalCatalan.fixedGaussianZeroState1Row27 line 1417
  30. def OAI.InternalCatalan.fixedGaussianZeroState1Row28 line 1469
  31. def OAI.InternalCatalan.fixedGaussianZeroState1Row29 line 1521
  32. def OAI.InternalCatalan.fixedGaussianZeroState1Row30 line 1573
  33. def OAI.InternalCatalan.fixedGaussianZeroState1Row31 line 1625
  34. def OAI.InternalCatalan.fixedGaussianZeroState1Row32 line 1677
  35. def OAI.InternalCatalan.fixedGaussianZeroState1Row33 line 1729
  36. def OAI.InternalCatalan.fixedGaussianZeroState1Row34 line 1781
  37. def OAI.InternalCatalan.fixedGaussianZeroState1Row35 line 1833
  38. def OAI.InternalCatalan.fixedGaussianZeroState1Row36 line 1885
  39. def OAI.InternalCatalan.fixedGaussianZeroState1Row37 line 1937
  40. def OAI.InternalCatalan.fixedGaussianZeroState1Row38 line 1989
  41. def OAI.InternalCatalan.fixedGaussianZeroState1Row39 line 2041
  42. def OAI.InternalCatalan.fixedGaussianZeroState1Row40 line 2093
  43. def OAI.InternalCatalan.fixedGaussianZeroState1Row41 line 2145
  44. def OAI.InternalCatalan.fixedGaussianZeroState1Row42 line 2197
  45. def OAI.InternalCatalan.fixedGaussianZeroState1Row43 line 2249
  46. def OAI.InternalCatalan.fixedGaussianZeroState1Row44 line 2301
  47. def OAI.InternalCatalan.fixedGaussianZeroState1Row45 line 2353
  48. def OAI.InternalCatalan.fixedGaussianZeroState1Row46 line 2405
  49. def OAI.InternalCatalan.fixedGaussianZeroState1Row47 line 2457
  50. def OAI.InternalCatalan.fixedGaussianZeroState1 line 2509
  51. theorem OAI.InternalCatalan.fixedGaussianZeroState0_eq line 2561
  52. theorem OAI.InternalCatalan.fixedGaussianZeroStep0_pivot line 2565
  53. theorem OAI.InternalCatalan.fixedGaussianZeroStep0_cells line 2577
  54. theorem OAI.InternalCatalan.fixedGaussianZeroStep0_eq line 2611