OAI/LinearAlgebra/MatrixFields/Certificates/Terminal4_3_1.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw line 26
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw_0_3_1 line 37
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw_1_2_1 line 41
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw_1_3_0 line 45
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw_2_1_1 line 49
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw_2_2_0 line 53
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw_3_0_1 line 57
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw_3_1_0 line 61
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw_4_0_0 line 65
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Raw_sound line 69
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Den line 82
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Den_sound line 83
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Den_positive line 85
15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Table line 86
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law line 97
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_check_0_3_1 line 98
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_check_1_2_1 line 99
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_check_1_3_0 line 100
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_check_2_1_1 line 101
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_check_2_2_0 line 102
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_check_3_0_1 line 103
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_check_3_1_0 line 104
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_check_4_0_0 line 105
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_check line 106
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Law_sound line 119
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Binary line 146
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Binary_eq line 152
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1LittleRat line 172
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Little line 177
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Little_sound line 181
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half line 189
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_0_0 line 208
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_0_1 line 212
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_0_2 line 216
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_0_3 line 220
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_0_4 line 224
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_0_5 line 228
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_1_0 line 232
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_1_1 line 236
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_1_2 line 240
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_1_3 line 244
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_1_4 line 248
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_1_5 line 252
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_2_0 line 256
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_2_1 line 260
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_2_2 line 264
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_2_3 line 268
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_2_4 line 272
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_check_2_5 line 276
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Half_sound line 280
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U0_3_1Leaf line 315
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U0_3_1Leaf_sound line 316
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U0_3_1Mass line 320
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U0_3_1Mass_sound line 321
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1D line 326
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1D_sound line 327
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1OneD line 330
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1OneD_sound line 331
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1EDLogWitness line 335
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1EDLog line 336
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1EDLog_sound line 337
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1ED line 341
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1ED_sound line 342
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1EOneDLogWitness line 344
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1EOneDLog line 345
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1EOneDLog_sound line 346
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1EOneD line 350
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1EOneD_sound line 351
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1BinaryEntropy line 353
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1BinaryEntropy_sound line 354
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1Leaf line 358
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1Leaf_sound line 359
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1Mass line 369
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_2_1Mass_sound line 370
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_3_0Leaf line 375
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_3_0Leaf_sound line 376
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_3_0Mass line 380
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U1_3_0Mass_sound line 381
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1D line 386
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1D_sound line 387
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1OneD line 390
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1OneD_sound line 391
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1EDLogWitness line 395
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1EDLog line 396
86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1EDLog_sound line 397
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1ED line 401
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1ED_sound line 402
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1EOneDLogWitness line 404
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1EOneDLog line 405
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1EOneDLog_sound line 406
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1EOneD line 410
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1EOneD_sound line 411
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1BinaryEntropy line 413
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1BinaryEntropy_sound line 414
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1Leaf line 418
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1Leaf_sound line 419
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1Mass line 429
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_1_1Mass_sound line 430
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0D line 435
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0D_sound line 436
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0OneD line 439
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0OneD_sound line 440
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0EDLogWitness line 444
105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0EDLog line 445
106. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0EDLog_sound line 446
107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0ED line 450
108. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0ED_sound line 451
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0EOneDLogWitness line 453
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0EOneDLog line 454
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0EOneDLog_sound line 455
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0EOneD line 459
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0EOneD_sound line 460
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0BinaryEntropy line 462
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0BinaryEntropy_sound line 463
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0Leaf line 467
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0Leaf_sound line 468
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0Mass line 476
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U2_2_0Mass_sound line 477
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U3_0_1Leaf line 482
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U3_0_1Leaf_sound line 483
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U3_0_1Mass line 487
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U3_0_1Mass_sound line 488
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U3_1_0Leaf line 493
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U3_1_0Leaf_sound line 494
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U3_1_0Mass line 498
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U3_1_0Mass_sound line 499
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U4_0_0Leaf line 504
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U4_0_0Leaf_sound line 505
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U4_0_0Mass line 509
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1U4_0_0Mass_sound line 510
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Leaves line 515
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Leaves_sound line 526
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Masses line 539
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Masses_sound line 550
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Binaries line 563
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1Binaries_sound line 569
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1S2 line 577
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B4_3_1S2_sound line 578