OAI/LinearAlgebra/MatrixFields/Certificates/Terminal3_4_1.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw line 26
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw_0_3_1 line 37
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw_0_4_0 line 41
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw_1_2_1 line 45
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw_1_3_0 line 49
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw_2_1_1 line 53
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw_2_2_0 line 57
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw_3_0_1 line 61
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw_3_1_0 line 65
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Raw_sound line 69
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Den line 82
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Den_sound line 83
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Den_positive line 85
15. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Table line 86
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law line 97
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_check_0_3_1 line 98
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_check_0_4_0 line 99
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_check_1_2_1 line 100
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_check_1_3_0 line 101
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_check_2_1_1 line 102
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_check_2_2_0 line 103
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_check_3_0_1 line 104
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_check_3_1_0 line 105
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_check line 106
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Law_sound line 119
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Binary line 146
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Binary_eq line 152
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1LittleRat line 172
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Little line 177
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Little_sound line 181
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half line 189
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_0_0 line 208
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_0_1 line 212
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_0_2 line 216
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_0_3 line 220
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_0_4 line 224
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_0_5 line 228
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_1_0 line 232
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_1_1 line 236
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_1_2 line 240
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_1_3 line 244
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_1_4 line 248
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_1_5 line 252
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_2_0 line 256
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_2_1 line 260
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_2_2 line 264
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_2_3 line 268
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_2_4 line 272
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_check_2_5 line 276
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Half_sound line 280
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U0_3_1Leaf line 315
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U0_3_1Leaf_sound line 316
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U0_3_1Mass line 321
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U0_3_1Mass_sound line 322
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U0_4_0Leaf line 327
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U0_4_0Leaf_sound line 328
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U0_4_0Mass line 333
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U0_4_0Mass_sound line 334
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1D line 339
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1D_sound line 340
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1OneD line 343
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1OneD_sound line 344
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1EDLogWitness line 348
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1EDLog line 349
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1EDLog_sound line 350
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1ED line 354
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1ED_sound line 355
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1EOneDLogWitness line 357
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1EOneDLog line 358
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1EOneDLog_sound line 359
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1EOneD line 363
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1EOneD_sound line 364
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1BinaryEntropy line 366
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1BinaryEntropy_sound line 367
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1Leaf line 371
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1Leaf_sound line 372
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1Mass line 383
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_2_1Mass_sound line 384
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_3_0Leaf line 389
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_3_0Leaf_sound line 390
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_3_0Mass line 395
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U1_3_0Mass_sound line 396
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1D line 401
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1D_sound line 402
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1OneD line 405
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1OneD_sound line 406
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1EDLogWitness line 410
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1EDLog line 411
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1EDLog_sound line 412
91. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1ED line 416
92. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1ED_sound line 417
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1EOneDLogWitness line 419
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1EOneDLog line 420
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1EOneDLog_sound line 421
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1EOneD line 425
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1EOneD_sound line 426
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1BinaryEntropy line 428
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1BinaryEntropy_sound line 429
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1Leaf line 433
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1Leaf_sound line 434
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1Mass line 445
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_1_1Mass_sound line 446
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0D line 451
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0D_sound line 452
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0OneD line 455
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0OneD_sound line 456
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0EDLogWitness line 460
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0EDLog line 461
110. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0EDLog_sound line 462
111. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0ED line 466
112. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0ED_sound line 467
113. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0EOneDLogWitness line 469
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0EOneDLog line 470
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0EOneDLog_sound line 471
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0EOneD line 475
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0EOneD_sound line 476
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0BinaryEntropy line 478
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0BinaryEntropy_sound line 479
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0Leaf line 483
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0Leaf_sound line 484
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0Mass line 492
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U2_2_0Mass_sound line 493
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U3_0_1Leaf line 498
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U3_0_1Leaf_sound line 499
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U3_0_1Mass line 504
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U3_0_1Mass_sound line 505
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U3_1_0Leaf line 510
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U3_1_0Leaf_sound line 511
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U3_1_0Mass line 516
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1U3_1_0Mass_sound line 517
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Leaves line 522
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Leaves_sound line 533
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Masses line 546
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Masses_sound line 557
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Binaries line 570
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1Binaries_sound line 576
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1S2 line 584
139. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_4_1S2_sound line 585