OAI/NumberTheory/Catalan/Determinants/ManuscriptNormRoundingVRow12.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.manuscriptNormV12_0SubstituteRat line 15
  2. theorem OAI.InternalCatalan.manuscriptNormV12_0SubstituteRat_interval line 18
  3. theorem OAI.InternalCatalan.manuscriptNormV12_0SubstituteRat_upper line 23
  4. def OAI.InternalCatalan.manuscriptNormV12_1SubstituteRat line 27
  5. theorem OAI.InternalCatalan.manuscriptNormV12_1SubstituteRat_interval line 30
  6. theorem OAI.InternalCatalan.manuscriptNormV12_1SubstituteRat_upper line 35
  7. def OAI.InternalCatalan.manuscriptNormV12_2SubstituteRat line 39
  8. theorem OAI.InternalCatalan.manuscriptNormV12_2SubstituteRat_interval line 42
  9. theorem OAI.InternalCatalan.manuscriptNormV12_2SubstituteRat_upper line 47
  10. def OAI.InternalCatalan.manuscriptNormV12_3SubstituteRat line 51
  11. theorem OAI.InternalCatalan.manuscriptNormV12_3SubstituteRat_interval line 54
  12. theorem OAI.InternalCatalan.manuscriptNormV12_3SubstituteRat_upper line 59
  13. def OAI.InternalCatalan.manuscriptNormV12_4SubstituteRat line 63
  14. theorem OAI.InternalCatalan.manuscriptNormV12_4SubstituteRat_interval line 66
  15. theorem OAI.InternalCatalan.manuscriptNormV12_4SubstituteRat_upper line 71
  16. def OAI.InternalCatalan.manuscriptNormV12_5SubstituteRat line 75
  17. theorem OAI.InternalCatalan.manuscriptNormV12_5SubstituteRat_interval line 78
  18. theorem OAI.InternalCatalan.manuscriptNormV12_5SubstituteRat_upper line 83
  19. def OAI.InternalCatalan.manuscriptNormV12_6SubstituteRat line 87
  20. theorem OAI.InternalCatalan.manuscriptNormV12_6SubstituteRat_interval line 90
  21. theorem OAI.InternalCatalan.manuscriptNormV12_6SubstituteRat_upper line 95
  22. def OAI.InternalCatalan.manuscriptNormV12_7SubstituteRat line 99
  23. theorem OAI.InternalCatalan.manuscriptNormV12_7SubstituteRat_interval line 102
  24. theorem OAI.InternalCatalan.manuscriptNormV12_7SubstituteRat_upper line 107
  25. def OAI.InternalCatalan.manuscriptNormV12_8SubstituteRat line 111
  26. theorem OAI.InternalCatalan.manuscriptNormV12_8SubstituteRat_interval line 114
  27. theorem OAI.InternalCatalan.manuscriptNormV12_8SubstituteRat_upper line 119
  28. def OAI.InternalCatalan.manuscriptNormV12_9SubstituteRat line 123
  29. theorem OAI.InternalCatalan.manuscriptNormV12_9SubstituteRat_interval line 126
  30. theorem OAI.InternalCatalan.manuscriptNormV12_9SubstituteRat_upper line 131
  31. def OAI.InternalCatalan.manuscriptNormV12_10SubstituteRat line 135
  32. theorem OAI.InternalCatalan.manuscriptNormV12_10SubstituteRat_interval line 138
  33. theorem OAI.InternalCatalan.manuscriptNormV12_10SubstituteRat_upper line 143
  34. def OAI.InternalCatalan.manuscriptNormV12_11SubstituteRat line 147
  35. theorem OAI.InternalCatalan.manuscriptNormV12_11SubstituteRat_interval line 150
  36. theorem OAI.InternalCatalan.manuscriptNormV12_11SubstituteRat_upper line 155
  37. def OAI.InternalCatalan.manuscriptNormV12_12SubstituteRat line 159
  38. theorem OAI.InternalCatalan.manuscriptNormV12_12SubstituteRat_interval line 162
  39. theorem OAI.InternalCatalan.manuscriptNormV12_12SubstituteRat_upper line 167
  40. def OAI.InternalCatalan.manuscriptNormVSubstituteRow12 line 171
  41. theorem OAI.InternalCatalan.manuscriptNormVSubstituteRow12_upper line 186
  42. theorem OAI.InternalCatalan.manuscriptNormV12_0SubstituteRat_composition_error line 212
  43. theorem OAI.InternalCatalan.manuscriptNormV12_1SubstituteRat_composition_error line 224
  44. theorem OAI.InternalCatalan.manuscriptNormV12_2SubstituteRat_composition_error line 236
  45. theorem OAI.InternalCatalan.manuscriptNormV12_3SubstituteRat_composition_error line 248
  46. theorem OAI.InternalCatalan.manuscriptNormV12_4SubstituteRat_composition_error line 260
  47. theorem OAI.InternalCatalan.manuscriptNormV12_5SubstituteRat_composition_error line 272
  48. theorem OAI.InternalCatalan.manuscriptNormV12_6SubstituteRat_composition_error line 284
  49. theorem OAI.InternalCatalan.manuscriptNormV12_7SubstituteRat_composition_error line 296
  50. theorem OAI.InternalCatalan.manuscriptNormV12_8SubstituteRat_composition_error line 308
  51. theorem OAI.InternalCatalan.manuscriptNormV12_9SubstituteRat_composition_error line 320
  52. theorem OAI.InternalCatalan.manuscriptNormV12_10SubstituteRat_composition_error line 332
  53. theorem OAI.InternalCatalan.manuscriptNormV12_11SubstituteRat_composition_error line 344
  54. theorem OAI.InternalCatalan.manuscriptNormV12_12SubstituteRat_composition_error line 356
  55. theorem OAI.InternalCatalan.manuscriptNormVCompositionRow12_error line 368
  56. def OAI.InternalCatalan.manuscriptNormV12_0RoundedSubstituteRat line 427
  57. theorem OAI.InternalCatalan.manuscriptNormV12_0RoundedSubstituteRat_error line 430
  58. def OAI.InternalCatalan.manuscriptNormV12_1RoundedSubstituteRat line 440
  59. theorem OAI.InternalCatalan.manuscriptNormV12_1RoundedSubstituteRat_error line 443
  60. def OAI.InternalCatalan.manuscriptNormV12_2RoundedSubstituteRat line 453
  61. theorem OAI.InternalCatalan.manuscriptNormV12_2RoundedSubstituteRat_error line 456
  62. def OAI.InternalCatalan.manuscriptNormV12_3RoundedSubstituteRat line 466
  63. theorem OAI.InternalCatalan.manuscriptNormV12_3RoundedSubstituteRat_error line 469
  64. def OAI.InternalCatalan.manuscriptNormV12_4RoundedSubstituteRat line 479
  65. theorem OAI.InternalCatalan.manuscriptNormV12_4RoundedSubstituteRat_error line 482
  66. def OAI.InternalCatalan.manuscriptNormV12_5RoundedSubstituteRat line 492
  67. theorem OAI.InternalCatalan.manuscriptNormV12_5RoundedSubstituteRat_error line 495
  68. def OAI.InternalCatalan.manuscriptNormV12_6RoundedSubstituteRat line 505
  69. theorem OAI.InternalCatalan.manuscriptNormV12_6RoundedSubstituteRat_error line 508
  70. def OAI.InternalCatalan.manuscriptNormV12_7RoundedSubstituteRat line 518
  71. theorem OAI.InternalCatalan.manuscriptNormV12_7RoundedSubstituteRat_error line 521
  72. def OAI.InternalCatalan.manuscriptNormV12_8RoundedSubstituteRat line 531
  73. theorem OAI.InternalCatalan.manuscriptNormV12_8RoundedSubstituteRat_error line 534
  74. def OAI.InternalCatalan.manuscriptNormV12_9RoundedSubstituteRat line 544
  75. theorem OAI.InternalCatalan.manuscriptNormV12_9RoundedSubstituteRat_error line 547
  76. def OAI.InternalCatalan.manuscriptNormV12_10RoundedSubstituteRat line 557
  77. theorem OAI.InternalCatalan.manuscriptNormV12_10RoundedSubstituteRat_error line 560
  78. def OAI.InternalCatalan.manuscriptNormV12_11RoundedSubstituteRat line 570
  79. theorem OAI.InternalCatalan.manuscriptNormV12_11RoundedSubstituteRat_error line 573
  80. def OAI.InternalCatalan.manuscriptNormV12_12RoundedSubstituteRat line 583
  81. theorem OAI.InternalCatalan.manuscriptNormV12_12RoundedSubstituteRat_error line 586
  82. def OAI.InternalCatalan.manuscriptNormVRoundedSubstituteRow12 line 596
  83. theorem OAI.InternalCatalan.manuscriptNormVRoundedRow12_error line 611