OAI/LinearAlgebra/MatrixFields/Certificates/Terminal3_1_4.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw line 26
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw_0_0_4 line 37
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw_0_1_3 line 41
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw_1_0_3 line 45
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw_1_1_2 line 49
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw_2_0_2 line 53
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw_2_1_1 line 57
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw_3_0_1 line 61
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw_3_1_0 line 65
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Raw_sound line 69
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Den line 82
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Den_sound line 83
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Den_positive line 85
15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Table line 86
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law line 97
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_check_0_0_4 line 98
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_check_0_1_3 line 99
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_check_1_0_3 line 100
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_check_1_1_2 line 101
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_check_2_0_2 line 102
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_check_2_1_1 line 103
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_check_3_0_1 line 104
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_check_3_1_0 line 105
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_check line 106
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Law_sound line 119
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Binary line 146
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Binary_eq line 152
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4LittleRat line 172
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Little line 177
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Little_sound line 181
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half line 189
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_0_0 line 208
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_0_1 line 212
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_0_2 line 216
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_0_3 line 220
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_0_4 line 224
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_0_5 line 228
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_1_0 line 232
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_1_1 line 236
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_1_2 line 240
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_1_3 line 244
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_1_4 line 248
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_1_5 line 252
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_2_0 line 256
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_2_1 line 260
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_2_2 line 264
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_2_3 line 268
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_2_4 line 272
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_check_2_5 line 276
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Half_sound line 280
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U0_0_4Leaf line 315
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U0_0_4Leaf_sound line 316
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U0_0_4Mass line 320
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U0_0_4Mass_sound line 321
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U0_1_3Leaf line 326
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U0_1_3Leaf_sound line 327
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U0_1_3Mass line 331
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U0_1_3Mass_sound line 332
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_0_3Leaf line 337
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_0_3Leaf_sound line 338
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_0_3Mass line 342
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_0_3Mass_sound line 343
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2D line 348
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2D_sound line 349
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2OneD line 352
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2OneD_sound line 353
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2EDLogWitness line 357
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2EDLog line 358
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2EDLog_sound line 359
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2ED line 363
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2ED_sound line 364
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2EOneDLogWitness line 366
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2EOneDLog line 367
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2EOneDLog_sound line 368
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2EOneD line 372
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2EOneD_sound line 373
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2BinaryEntropy line 375
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2BinaryEntropy_sound line 376
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2Leaf line 380
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2Leaf_sound line 381
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2Mass line 392
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U1_1_2Mass_sound line 393
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2D line 398
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2D_sound line 399
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2OneD line 402
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2OneD_sound line 403
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2EDLogWitness line 407
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2EDLog line 408
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2EDLog_sound line 409
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2ED line 413
92. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2ED_sound line 414
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2EOneDLogWitness line 416
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2EOneDLog line 417
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2EOneDLog_sound line 418
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2EOneD line 422
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2EOneD_sound line 423
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2BinaryEntropy line 425
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2BinaryEntropy_sound line 426
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2Leaf line 430
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2Leaf_sound line 431
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2Mass line 439
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_0_2Mass_sound line 440
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1D line 445
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1D_sound line 446
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1OneD line 449
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1OneD_sound line 450
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1EDLogWitness line 454
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1EDLog line 455
110. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1EDLog_sound line 456
111. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1ED line 460
112. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1ED_sound line 461
113. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1EOneDLogWitness line 463
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1EOneDLog line 464
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1EOneDLog_sound line 465
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1EOneD line 469
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1EOneD_sound line 470
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1BinaryEntropy line 472
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1BinaryEntropy_sound line 473
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1Leaf line 477
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1Leaf_sound line 478
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1Mass line 489
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U2_1_1Mass_sound line 490
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U3_0_1Leaf line 495
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U3_0_1Leaf_sound line 496
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U3_0_1Mass line 500
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U3_0_1Mass_sound line 501
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U3_1_0Leaf line 506
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U3_1_0Leaf_sound line 507
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U3_1_0Mass line 511
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4U3_1_0Mass_sound line 512
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Leaves line 517
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Leaves_sound line 528
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Masses line 541
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Masses_sound line 552
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Binaries line 565
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4Binaries_sound line 571
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4S2 line 579
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_1_4S2_sound line 580