OAI/NumberTheory/Catalan/FiniteMatrices/FixedGaussianMinusStep0.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.fixedGaussianMinusState0 line 10
  2. def OAI.InternalCatalan.fixedGaussianMinusState1Row0 line 13
  3. def OAI.InternalCatalan.fixedGaussianMinusState1Row1 line 65
  4. def OAI.InternalCatalan.fixedGaussianMinusState1Row2 line 117
  5. def OAI.InternalCatalan.fixedGaussianMinusState1Row3 line 169
  6. def OAI.InternalCatalan.fixedGaussianMinusState1Row4 line 221
  7. def OAI.InternalCatalan.fixedGaussianMinusState1Row5 line 273
  8. def OAI.InternalCatalan.fixedGaussianMinusState1Row6 line 325
  9. def OAI.InternalCatalan.fixedGaussianMinusState1Row7 line 377
  10. def OAI.InternalCatalan.fixedGaussianMinusState1Row8 line 429
  11. def OAI.InternalCatalan.fixedGaussianMinusState1Row9 line 481
  12. def OAI.InternalCatalan.fixedGaussianMinusState1Row10 line 533
  13. def OAI.InternalCatalan.fixedGaussianMinusState1Row11 line 585
  14. def OAI.InternalCatalan.fixedGaussianMinusState1Row12 line 637
  15. def OAI.InternalCatalan.fixedGaussianMinusState1Row13 line 689
  16. def OAI.InternalCatalan.fixedGaussianMinusState1Row14 line 741
  17. def OAI.InternalCatalan.fixedGaussianMinusState1Row15 line 793
  18. def OAI.InternalCatalan.fixedGaussianMinusState1Row16 line 845
  19. def OAI.InternalCatalan.fixedGaussianMinusState1Row17 line 897
  20. def OAI.InternalCatalan.fixedGaussianMinusState1Row18 line 949
  21. def OAI.InternalCatalan.fixedGaussianMinusState1Row19 line 1001
  22. def OAI.InternalCatalan.fixedGaussianMinusState1Row20 line 1053
  23. def OAI.InternalCatalan.fixedGaussianMinusState1Row21 line 1105
  24. def OAI.InternalCatalan.fixedGaussianMinusState1Row22 line 1157
  25. def OAI.InternalCatalan.fixedGaussianMinusState1Row23 line 1209
  26. def OAI.InternalCatalan.fixedGaussianMinusState1Row24 line 1261
  27. def OAI.InternalCatalan.fixedGaussianMinusState1Row25 line 1313
  28. def OAI.InternalCatalan.fixedGaussianMinusState1Row26 line 1365
  29. def OAI.InternalCatalan.fixedGaussianMinusState1Row27 line 1417
  30. def OAI.InternalCatalan.fixedGaussianMinusState1Row28 line 1469
  31. def OAI.InternalCatalan.fixedGaussianMinusState1Row29 line 1521
  32. def OAI.InternalCatalan.fixedGaussianMinusState1Row30 line 1573
  33. def OAI.InternalCatalan.fixedGaussianMinusState1Row31 line 1625
  34. def OAI.InternalCatalan.fixedGaussianMinusState1Row32 line 1677
  35. def OAI.InternalCatalan.fixedGaussianMinusState1Row33 line 1729
  36. def OAI.InternalCatalan.fixedGaussianMinusState1Row34 line 1781
  37. def OAI.InternalCatalan.fixedGaussianMinusState1Row35 line 1833
  38. def OAI.InternalCatalan.fixedGaussianMinusState1Row36 line 1885
  39. def OAI.InternalCatalan.fixedGaussianMinusState1Row37 line 1937
  40. def OAI.InternalCatalan.fixedGaussianMinusState1Row38 line 1989
  41. def OAI.InternalCatalan.fixedGaussianMinusState1Row39 line 2041
  42. def OAI.InternalCatalan.fixedGaussianMinusState1Row40 line 2093
  43. def OAI.InternalCatalan.fixedGaussianMinusState1Row41 line 2145
  44. def OAI.InternalCatalan.fixedGaussianMinusState1Row42 line 2197
  45. def OAI.InternalCatalan.fixedGaussianMinusState1Row43 line 2249
  46. def OAI.InternalCatalan.fixedGaussianMinusState1Row44 line 2301
  47. def OAI.InternalCatalan.fixedGaussianMinusState1Row45 line 2353
  48. def OAI.InternalCatalan.fixedGaussianMinusState1Row46 line 2405
  49. def OAI.InternalCatalan.fixedGaussianMinusState1Row47 line 2457
  50. def OAI.InternalCatalan.fixedGaussianMinusState1 line 2509
  51. theorem OAI.InternalCatalan.fixedGaussianMinusState0_eq line 2561
  52. theorem OAI.InternalCatalan.fixedGaussianMinusStep0_pivot line 2565
  53. theorem OAI.InternalCatalan.fixedGaussianMinusStep0_cells line 2577
  54. theorem OAI.InternalCatalan.fixedGaussianMinusStep0_eq line 2611