OAI/NumberTheory/Catalan/Determinants/ManuscriptNormRoundingVRow08.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptNormV8_0SubstituteRat line 16
  2. theorem OAI.InternalCatalan.manuscriptNormV8_0SubstituteRat_interval line 19
  3. theorem OAI.InternalCatalan.manuscriptNormV8_0SubstituteRat_upper line 24
  4. def OAI.InternalCatalan.manuscriptNormV8_1SubstituteRat line 28
  5. theorem OAI.InternalCatalan.manuscriptNormV8_1SubstituteRat_interval line 31
  6. theorem OAI.InternalCatalan.manuscriptNormV8_1SubstituteRat_upper line 36
  7. def OAI.InternalCatalan.manuscriptNormV8_2SubstituteRat line 40
  8. theorem OAI.InternalCatalan.manuscriptNormV8_2SubstituteRat_interval line 43
  9. theorem OAI.InternalCatalan.manuscriptNormV8_2SubstituteRat_upper line 48
  10. def OAI.InternalCatalan.manuscriptNormV8_3SubstituteRat line 52
  11. theorem OAI.InternalCatalan.manuscriptNormV8_3SubstituteRat_interval line 55
  12. theorem OAI.InternalCatalan.manuscriptNormV8_3SubstituteRat_upper line 60
  13. def OAI.InternalCatalan.manuscriptNormV8_4SubstituteRat line 64
  14. theorem OAI.InternalCatalan.manuscriptNormV8_4SubstituteRat_interval line 67
  15. theorem OAI.InternalCatalan.manuscriptNormV8_4SubstituteRat_upper line 72
  16. def OAI.InternalCatalan.manuscriptNormV8_5SubstituteRat line 76
  17. theorem OAI.InternalCatalan.manuscriptNormV8_5SubstituteRat_interval line 79
  18. theorem OAI.InternalCatalan.manuscriptNormV8_5SubstituteRat_upper line 84
  19. def OAI.InternalCatalan.manuscriptNormV8_6SubstituteRat line 88
  20. theorem OAI.InternalCatalan.manuscriptNormV8_6SubstituteRat_interval line 91
  21. theorem OAI.InternalCatalan.manuscriptNormV8_6SubstituteRat_upper line 96
  22. def OAI.InternalCatalan.manuscriptNormV8_7SubstituteRat line 100
  23. theorem OAI.InternalCatalan.manuscriptNormV8_7SubstituteRat_interval line 103
  24. theorem OAI.InternalCatalan.manuscriptNormV8_7SubstituteRat_upper line 108
  25. def OAI.InternalCatalan.manuscriptNormV8_8SubstituteRat line 112
  26. theorem OAI.InternalCatalan.manuscriptNormV8_8SubstituteRat_interval line 115
  27. theorem OAI.InternalCatalan.manuscriptNormV8_8SubstituteRat_upper line 120
  28. def OAI.InternalCatalan.manuscriptNormV8_9SubstituteRat line 124
  29. theorem OAI.InternalCatalan.manuscriptNormV8_9SubstituteRat_interval line 127
  30. theorem OAI.InternalCatalan.manuscriptNormV8_9SubstituteRat_upper line 132
  31. def OAI.InternalCatalan.manuscriptNormV8_10SubstituteRat line 136
  32. theorem OAI.InternalCatalan.manuscriptNormV8_10SubstituteRat_interval line 139
  33. theorem OAI.InternalCatalan.manuscriptNormV8_10SubstituteRat_upper line 144
  34. def OAI.InternalCatalan.manuscriptNormV8_11SubstituteRat line 148
  35. theorem OAI.InternalCatalan.manuscriptNormV8_11SubstituteRat_interval line 151
  36. theorem OAI.InternalCatalan.manuscriptNormV8_11SubstituteRat_upper line 156
  37. def OAI.InternalCatalan.manuscriptNormV8_12SubstituteRat line 160
  38. theorem OAI.InternalCatalan.manuscriptNormV8_12SubstituteRat_interval line 163
  39. theorem OAI.InternalCatalan.manuscriptNormV8_12SubstituteRat_upper line 168
  40. def OAI.InternalCatalan.manuscriptNormVSubstituteRow8 line 172
  41. theorem OAI.InternalCatalan.manuscriptNormVSubstituteRow8_upper line 187
  42. theorem OAI.InternalCatalan.manuscriptNormV8_0SubstituteRat_composition_error line 213
  43. theorem OAI.InternalCatalan.manuscriptNormV8_1SubstituteRat_composition_error line 225
  44. theorem OAI.InternalCatalan.manuscriptNormV8_2SubstituteRat_composition_error line 237
  45. theorem OAI.InternalCatalan.manuscriptNormV8_3SubstituteRat_composition_error line 249
  46. theorem OAI.InternalCatalan.manuscriptNormV8_4SubstituteRat_composition_error line 261
  47. theorem OAI.InternalCatalan.manuscriptNormV8_5SubstituteRat_composition_error line 273
  48. theorem OAI.InternalCatalan.manuscriptNormV8_6SubstituteRat_composition_error line 285
  49. theorem OAI.InternalCatalan.manuscriptNormV8_7SubstituteRat_composition_error line 297
  50. theorem OAI.InternalCatalan.manuscriptNormV8_8SubstituteRat_composition_error line 309
  51. theorem OAI.InternalCatalan.manuscriptNormV8_9SubstituteRat_composition_error line 321
  52. theorem OAI.InternalCatalan.manuscriptNormV8_10SubstituteRat_composition_error line 333
  53. theorem OAI.InternalCatalan.manuscriptNormV8_11SubstituteRat_composition_error line 345
  54. theorem OAI.InternalCatalan.manuscriptNormV8_12SubstituteRat_composition_error line 357
  55. theorem OAI.InternalCatalan.manuscriptNormVCompositionRow8_error line 369
  56. def OAI.InternalCatalan.manuscriptNormV8_0RoundedSubstituteRat line 428
  57. theorem OAI.InternalCatalan.manuscriptNormV8_0RoundedSubstituteRat_error line 431
  58. def OAI.InternalCatalan.manuscriptNormV8_1RoundedSubstituteRat line 441
  59. theorem OAI.InternalCatalan.manuscriptNormV8_1RoundedSubstituteRat_error line 444
  60. def OAI.InternalCatalan.manuscriptNormV8_2RoundedSubstituteRat line 454
  61. theorem OAI.InternalCatalan.manuscriptNormV8_2RoundedSubstituteRat_error line 457
  62. def OAI.InternalCatalan.manuscriptNormV8_3RoundedSubstituteRat line 467
  63. theorem OAI.InternalCatalan.manuscriptNormV8_3RoundedSubstituteRat_error line 470
  64. def OAI.InternalCatalan.manuscriptNormV8_4RoundedSubstituteRat line 480
  65. theorem OAI.InternalCatalan.manuscriptNormV8_4RoundedSubstituteRat_error line 483
  66. def OAI.InternalCatalan.manuscriptNormV8_5RoundedSubstituteRat line 493
  67. theorem OAI.InternalCatalan.manuscriptNormV8_5RoundedSubstituteRat_error line 496
  68. def OAI.InternalCatalan.manuscriptNormV8_6RoundedSubstituteRat line 506
  69. theorem OAI.InternalCatalan.manuscriptNormV8_6RoundedSubstituteRat_error line 509
  70. def OAI.InternalCatalan.manuscriptNormV8_7RoundedSubstituteRat line 519
  71. theorem OAI.InternalCatalan.manuscriptNormV8_7RoundedSubstituteRat_error line 522
  72. def OAI.InternalCatalan.manuscriptNormV8_8RoundedSubstituteRat line 532
  73. theorem OAI.InternalCatalan.manuscriptNormV8_8RoundedSubstituteRat_error line 535
  74. def OAI.InternalCatalan.manuscriptNormV8_9RoundedSubstituteRat line 545
  75. theorem OAI.InternalCatalan.manuscriptNormV8_9RoundedSubstituteRat_error line 548
  76. def OAI.InternalCatalan.manuscriptNormV8_10RoundedSubstituteRat line 558
  77. theorem OAI.InternalCatalan.manuscriptNormV8_10RoundedSubstituteRat_error line 561
  78. def OAI.InternalCatalan.manuscriptNormV8_11RoundedSubstituteRat line 571
  79. theorem OAI.InternalCatalan.manuscriptNormV8_11RoundedSubstituteRat_error line 574
  80. def OAI.InternalCatalan.manuscriptNormV8_12RoundedSubstituteRat line 584
  81. theorem OAI.InternalCatalan.manuscriptNormV8_12RoundedSubstituteRat_error line 587
  82. def OAI.InternalCatalan.manuscriptNormVRoundedSubstituteRow8 line 597
  83. theorem OAI.InternalCatalan.manuscriptNormVRoundedRow8_error line 612