OAI/LinearAlgebra/MatrixFields/Certificates/Terminal4_1_3.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw line 26
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw_0_1_3 line 37
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw_1_0_3 line 41
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw_1_1_2 line 45
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw_2_0_2 line 49
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw_2_1_1 line 53
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw_3_0_1 line 57
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw_3_1_0 line 61
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw_4_0_0 line 65
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Raw_sound line 69
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Den line 82
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Den_sound line 83
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Den_positive line 85
15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Table line 86
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law line 97
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_check_0_1_3 line 98
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_check_1_0_3 line 99
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_check_1_1_2 line 100
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_check_2_0_2 line 101
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_check_2_1_1 line 102
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_check_3_0_1 line 103
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_check_3_1_0 line 104
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_check_4_0_0 line 105
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_check line 106
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Law_sound line 119
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Binary line 146
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Binary_eq line 152
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3LittleRat line 172
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Little line 177
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Little_sound line 181
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half line 189
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_0_0 line 208
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_0_1 line 212
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_0_2 line 216
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_0_3 line 220
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_0_4 line 224
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_0_5 line 228
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_1_0 line 232
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_1_1 line 236
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_1_2 line 240
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_1_3 line 244
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_1_4 line 248
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_1_5 line 252
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_2_0 line 256
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_2_1 line 260
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_2_2 line 264
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_2_3 line 268
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_2_4 line 272
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_check_2_5 line 276
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Half_sound line 280
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U0_1_3Leaf line 315
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U0_1_3Leaf_sound line 316
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U0_1_3Mass line 320
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U0_1_3Mass_sound line 321
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_0_3Leaf line 326
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_0_3Leaf_sound line 327
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_0_3Mass line 331
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_0_3Mass_sound line 332
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2D line 337
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2D_sound line 338
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2OneD line 341
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2OneD_sound line 342
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2EDLogWitness line 346
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2EDLog line 347
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2EDLog_sound line 348
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2ED line 352
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2ED_sound line 353
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2EOneDLogWitness line 355
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2EOneDLog line 356
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2EOneDLog_sound line 357
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2EOneD line 361
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2EOneD_sound line 362
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2BinaryEntropy line 364
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2BinaryEntropy_sound line 365
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2Leaf line 369
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2Leaf_sound line 370
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2Mass line 381
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U1_1_2Mass_sound line 382
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2D line 387
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2D_sound line 388
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2OneD line 391
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2OneD_sound line 392
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2EDLogWitness line 396
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2EDLog line 397
86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2EDLog_sound line 398
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2ED line 402
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2ED_sound line 403
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2EOneDLogWitness line 405
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2EOneDLog line 406
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2EOneDLog_sound line 407
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2EOneD line 411
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2EOneD_sound line 412
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2BinaryEntropy line 414
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2BinaryEntropy_sound line 415
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2Leaf line 419
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2Leaf_sound line 420
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2Mass line 428
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_0_2Mass_sound line 429
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1D line 434
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1D_sound line 435
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1OneD line 438
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1OneD_sound line 439
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1EDLogWitness line 443
105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1EDLog line 444
106. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1EDLog_sound line 445
107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1ED line 449
108. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1ED_sound line 450
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1EOneDLogWitness line 452
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1EOneDLog line 453
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1EOneDLog_sound line 454
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1EOneD line 458
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1EOneD_sound line 459
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1BinaryEntropy line 461
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1BinaryEntropy_sound line 462
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1Leaf line 466
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1Leaf_sound line 467
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1Mass line 478
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U2_1_1Mass_sound line 479
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U3_0_1Leaf line 484
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U3_0_1Leaf_sound line 485
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U3_0_1Mass line 489
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U3_0_1Mass_sound line 490
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U3_1_0Leaf line 495
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U3_1_0Leaf_sound line 496
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U3_1_0Mass line 500
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U3_1_0Mass_sound line 501
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U4_0_0Leaf line 506
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U4_0_0Leaf_sound line 507
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U4_0_0Mass line 511
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3U4_0_0Mass_sound line 512
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Leaves line 517
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Leaves_sound line 528
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Masses line 541
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Masses_sound line 552
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Binaries line 565
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3Binaries_sound line 571
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3S2 line 579
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_1_3S2_sound line 580