OAI/Analysis/Quantum/DimensionTen/EigenData.lean

GitHub source file

182 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DimensionTen.Border.mon_product_0_0 line 10
  2. lemma OAI.DimensionTen.Border.column_0_0 line 14
  3. lemma OAI.DimensionTen.Border.NB_column_0_0 line 16
  4. lemma OAI.DimensionTen.Border.mon_product_0_1 line 19
  5. lemma OAI.DimensionTen.Border.column_0_1 line 23
  6. lemma OAI.DimensionTen.Border.NB_column_0_1 line 25
  7. lemma OAI.DimensionTen.Border.mon_product_0_2 line 28
  8. lemma OAI.DimensionTen.Border.column_0_2 line 32
  9. lemma OAI.DimensionTen.Border.NB_column_0_2 line 34
  10. lemma OAI.DimensionTen.Border.mon_product_0_3 line 37
  11. lemma OAI.DimensionTen.Border.column_0_3 line 42
  12. lemma OAI.DimensionTen.Border.NB_column_0_3 line 44
  13. lemma OAI.DimensionTen.Border.mon_product_0_4 line 47
  14. lemma OAI.DimensionTen.Border.column_0_4 line 51
  15. lemma OAI.DimensionTen.Border.NB_column_0_4 line 53
  16. lemma OAI.DimensionTen.Border.mon_product_0_5 line 56
  17. lemma OAI.DimensionTen.Border.column_0_5 line 60
  18. lemma OAI.DimensionTen.Border.NB_column_0_5 line 62
  19. lemma OAI.DimensionTen.Border.mon_product_0_6 line 65
  20. lemma OAI.DimensionTen.Border.column_0_6 line 69
  21. lemma OAI.DimensionTen.Border.NB_column_0_6 line 71
  22. lemma OAI.DimensionTen.Border.mon_product_0_7 line 74
  23. lemma OAI.DimensionTen.Border.column_0_7 line 79
  24. lemma OAI.DimensionTen.Border.NB_column_0_7 line 81
  25. lemma OAI.DimensionTen.Border.mon_product_0_8 line 84
  26. lemma OAI.DimensionTen.Border.column_0_8 line 89
  27. lemma OAI.DimensionTen.Border.NB_column_0_8 line 91
  28. lemma OAI.DimensionTen.Border.mon_product_0_9 line 94
  29. lemma OAI.DimensionTen.Border.column_0_9 line 99
  30. lemma OAI.DimensionTen.Border.NB_column_0_9 line 101
  31. lemma OAI.DimensionTen.Border.mon_product_0_10 line 104
  32. lemma OAI.DimensionTen.Border.column_0_10 line 108
  33. lemma OAI.DimensionTen.Border.NB_column_0_10 line 110
  34. lemma OAI.DimensionTen.Border.mon_product_0_11 line 113
  35. lemma OAI.DimensionTen.Border.column_0_11 line 117
  36. lemma OAI.DimensionTen.Border.NB_column_0_11 line 119
  37. lemma OAI.DimensionTen.Border.mon_product_0_12 line 122
  38. lemma OAI.DimensionTen.Border.column_0_12 line 126
  39. lemma OAI.DimensionTen.Border.NB_column_0_12 line 128
  40. lemma OAI.DimensionTen.Border.mon_product_0_13 line 131
  41. lemma OAI.DimensionTen.Border.column_0_13 line 135
  42. lemma OAI.DimensionTen.Border.NB_column_0_13 line 137
  43. lemma OAI.DimensionTen.Border.mon_product_0_14 line 140
  44. lemma OAI.DimensionTen.Border.column_0_14 line 145
  45. lemma OAI.DimensionTen.Border.NB_column_0_14 line 147
  46. lemma OAI.DimensionTen.Border.mon_product_0_15 line 150
  47. lemma OAI.DimensionTen.Border.column_0_15 line 155
  48. lemma OAI.DimensionTen.Border.NB_column_0_15 line 157
  49. lemma OAI.DimensionTen.Border.mon_product_0_16 line 160
  50. lemma OAI.DimensionTen.Border.column_0_16 line 165
  51. lemma OAI.DimensionTen.Border.NB_column_0_16 line 167
  52. lemma OAI.DimensionTen.Border.mon_product_0_17 line 170
  53. lemma OAI.DimensionTen.Border.column_0_17 line 175
  54. lemma OAI.DimensionTen.Border.NB_column_0_17 line 177
  55. lemma OAI.DimensionTen.Border.mon_product_0_18 line 180
  56. lemma OAI.DimensionTen.Border.column_0_18 line 185
  57. lemma OAI.DimensionTen.Border.NB_column_0_18 line 187
  58. lemma OAI.DimensionTen.Border.mon_product_0_19 line 190
  59. lemma OAI.DimensionTen.Border.column_0_19 line 195
  60. lemma OAI.DimensionTen.Border.NB_column_0_19 line 197
  61. lemma OAI.DimensionTen.Border.mon_product_1_0 line 200
  62. lemma OAI.DimensionTen.Border.column_1_0 line 204
  63. lemma OAI.DimensionTen.Border.NB_column_1_0 line 206
  64. lemma OAI.DimensionTen.Border.mon_product_1_1 line 209
  65. lemma OAI.DimensionTen.Border.column_1_1 line 213
  66. lemma OAI.DimensionTen.Border.NB_column_1_1 line 215
  67. lemma OAI.DimensionTen.Border.mon_product_1_2 line 218
  68. lemma OAI.DimensionTen.Border.column_1_2 line 223
  69. lemma OAI.DimensionTen.Border.NB_column_1_2 line 225
  70. lemma OAI.DimensionTen.Border.mon_product_1_3 line 228
  71. lemma OAI.DimensionTen.Border.column_1_3 line 233
  72. lemma OAI.DimensionTen.Border.NB_column_1_3 line 235
  73. lemma OAI.DimensionTen.Border.mon_product_1_4 line 238
  74. lemma OAI.DimensionTen.Border.column_1_4 line 242
  75. lemma OAI.DimensionTen.Border.NB_column_1_4 line 244
  76. lemma OAI.DimensionTen.Border.mon_product_1_5 line 247
  77. lemma OAI.DimensionTen.Border.column_1_5 line 252
  78. lemma OAI.DimensionTen.Border.NB_column_1_5 line 254
  79. lemma OAI.DimensionTen.Border.mon_product_1_6 line 257
  80. lemma OAI.DimensionTen.Border.column_1_6 line 262
  81. lemma OAI.DimensionTen.Border.NB_column_1_6 line 264
  82. lemma OAI.DimensionTen.Border.mon_product_1_7 line 267
  83. lemma OAI.DimensionTen.Border.column_1_7 line 272
  84. lemma OAI.DimensionTen.Border.NB_column_1_7 line 274
  85. lemma OAI.DimensionTen.Border.mon_product_1_8 line 277
  86. lemma OAI.DimensionTen.Border.column_1_8 line 282
  87. lemma OAI.DimensionTen.Border.NB_column_1_8 line 284
  88. lemma OAI.DimensionTen.Border.mon_product_1_9 line 287
  89. lemma OAI.DimensionTen.Border.column_1_9 line 292
  90. lemma OAI.DimensionTen.Border.NB_column_1_9 line 294
  91. lemma OAI.DimensionTen.Border.mon_product_1_10 line 297
  92. lemma OAI.DimensionTen.Border.column_1_10 line 301
  93. lemma OAI.DimensionTen.Border.NB_column_1_10 line 303
  94. lemma OAI.DimensionTen.Border.mon_product_1_11 line 306
  95. lemma OAI.DimensionTen.Border.column_1_11 line 311
  96. lemma OAI.DimensionTen.Border.NB_column_1_11 line 313
  97. lemma OAI.DimensionTen.Border.mon_product_1_12 line 316
  98. lemma OAI.DimensionTen.Border.column_1_12 line 321
  99. lemma OAI.DimensionTen.Border.NB_column_1_12 line 323
  100. lemma OAI.DimensionTen.Border.mon_product_1_13 line 326
  101. lemma OAI.DimensionTen.Border.column_1_13 line 331
  102. lemma OAI.DimensionTen.Border.NB_column_1_13 line 333
  103. lemma OAI.DimensionTen.Border.mon_product_1_14 line 336
  104. lemma OAI.DimensionTen.Border.column_1_14 line 341
  105. lemma OAI.DimensionTen.Border.NB_column_1_14 line 343
  106. lemma OAI.DimensionTen.Border.mon_product_1_15 line 346
  107. lemma OAI.DimensionTen.Border.column_1_15 line 351
  108. lemma OAI.DimensionTen.Border.NB_column_1_15 line 353
  109. lemma OAI.DimensionTen.Border.mon_product_1_16 line 356
  110. lemma OAI.DimensionTen.Border.column_1_16 line 361
  111. lemma OAI.DimensionTen.Border.NB_column_1_16 line 363
  112. lemma OAI.DimensionTen.Border.mon_product_1_17 line 366
  113. lemma OAI.DimensionTen.Border.column_1_17 line 371
  114. lemma OAI.DimensionTen.Border.NB_column_1_17 line 373
  115. lemma OAI.DimensionTen.Border.mon_product_1_18 line 376
  116. lemma OAI.DimensionTen.Border.column_1_18 line 381
  117. lemma OAI.DimensionTen.Border.NB_column_1_18 line 383
  118. lemma OAI.DimensionTen.Border.mon_product_1_19 line 386
  119. lemma OAI.DimensionTen.Border.column_1_19 line 391
  120. lemma OAI.DimensionTen.Border.NB_column_1_19 line 393
  121. lemma OAI.DimensionTen.Border.mon_product_2_0 line 396
  122. lemma OAI.DimensionTen.Border.column_2_0 line 400
  123. lemma OAI.DimensionTen.Border.NB_column_2_0 line 402
  124. lemma OAI.DimensionTen.Border.mon_product_2_1 line 405
  125. lemma OAI.DimensionTen.Border.column_2_1 line 410
  126. lemma OAI.DimensionTen.Border.NB_column_2_1 line 412
  127. lemma OAI.DimensionTen.Border.mon_product_2_2 line 415
  128. lemma OAI.DimensionTen.Border.column_2_2 line 420
  129. lemma OAI.DimensionTen.Border.NB_column_2_2 line 422
  130. lemma OAI.DimensionTen.Border.mon_product_2_3 line 425
  131. lemma OAI.DimensionTen.Border.column_2_3 line 430
  132. lemma OAI.DimensionTen.Border.NB_column_2_3 line 432
  133. lemma OAI.DimensionTen.Border.mon_product_2_4 line 435
  134. lemma OAI.DimensionTen.Border.column_2_4 line 440
  135. lemma OAI.DimensionTen.Border.NB_column_2_4 line 442
  136. lemma OAI.DimensionTen.Border.mon_product_2_5 line 445
  137. lemma OAI.DimensionTen.Border.column_2_5 line 450
  138. lemma OAI.DimensionTen.Border.NB_column_2_5 line 452
  139. lemma OAI.DimensionTen.Border.mon_product_2_6 line 455
  140. lemma OAI.DimensionTen.Border.column_2_6 line 460
  141. lemma OAI.DimensionTen.Border.NB_column_2_6 line 462
  142. lemma OAI.DimensionTen.Border.mon_product_2_7 line 465
  143. lemma OAI.DimensionTen.Border.column_2_7 line 470
  144. lemma OAI.DimensionTen.Border.NB_column_2_7 line 472
  145. lemma OAI.DimensionTen.Border.mon_product_2_8 line 475
  146. lemma OAI.DimensionTen.Border.column_2_8 line 480
  147. lemma OAI.DimensionTen.Border.NB_column_2_8 line 482
  148. lemma OAI.DimensionTen.Border.mon_product_2_9 line 485
  149. lemma OAI.DimensionTen.Border.column_2_9 line 490
  150. lemma OAI.DimensionTen.Border.NB_column_2_9 line 492
  151. lemma OAI.DimensionTen.Border.mon_product_2_10 line 495
  152. lemma OAI.DimensionTen.Border.column_2_10 line 500
  153. lemma OAI.DimensionTen.Border.NB_column_2_10 line 502
  154. lemma OAI.DimensionTen.Border.mon_product_2_11 line 505
  155. lemma OAI.DimensionTen.Border.column_2_11 line 510
  156. lemma OAI.DimensionTen.Border.NB_column_2_11 line 512
  157. lemma OAI.DimensionTen.Border.mon_product_2_12 line 515
  158. lemma OAI.DimensionTen.Border.column_2_12 line 520
  159. lemma OAI.DimensionTen.Border.NB_column_2_12 line 522
  160. lemma OAI.DimensionTen.Border.mon_product_2_13 line 525
  161. lemma OAI.DimensionTen.Border.column_2_13 line 530
  162. lemma OAI.DimensionTen.Border.NB_column_2_13 line 532
  163. lemma OAI.DimensionTen.Border.mon_product_2_14 line 535
  164. lemma OAI.DimensionTen.Border.column_2_14 line 540
  165. lemma OAI.DimensionTen.Border.NB_column_2_14 line 542
  166. lemma OAI.DimensionTen.Border.mon_product_2_15 line 545
  167. lemma OAI.DimensionTen.Border.column_2_15 line 550
  168. lemma OAI.DimensionTen.Border.NB_column_2_15 line 552
  169. lemma OAI.DimensionTen.Border.mon_product_2_16 line 555
  170. lemma OAI.DimensionTen.Border.column_2_16 line 560
  171. lemma OAI.DimensionTen.Border.NB_column_2_16 line 562
  172. lemma OAI.DimensionTen.Border.mon_product_2_17 line 565
  173. lemma OAI.DimensionTen.Border.column_2_17 line 570
  174. lemma OAI.DimensionTen.Border.NB_column_2_17 line 572
  175. lemma OAI.DimensionTen.Border.mon_product_2_18 line 575
  176. lemma OAI.DimensionTen.Border.column_2_18 line 580
  177. lemma OAI.DimensionTen.Border.NB_column_2_18 line 582
  178. lemma OAI.DimensionTen.Border.mon_product_2_19 line 585
  179. lemma OAI.DimensionTen.Border.column_2_19 line 590
  180. lemma OAI.DimensionTen.Border.NB_column_2_19 line 592
  181. lemma OAI.DimensionTen.Border.single_to_sum line 595
  182. lemma OAI.DimensionTen.Border.eigen_columns line 600