OAI/LinearAlgebra/MatrixFields/Certificates/Terminal5_2_1.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Raw line 24
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Raw_1_2_1 line 33
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Raw_2_1_1 line 37
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Raw_2_2_0 line 41
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Raw_3_0_1 line 45
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Raw_3_1_0 line 49
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Raw_4_0_0 line 53
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Raw_sound line 57
10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Den line 68
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Den_sound line 69
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Den_positive line 71
13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Table line 72
14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Law line 81
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Law_check_1_2_1 line 82
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Law_check_2_1_1 line 83
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Law_check_2_2_0 line 84
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Law_check_3_0_1 line 85
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Law_check_3_1_0 line 86
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Law_check_4_0_0 line 87
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Law_check line 88
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Law_sound line 99
23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Binary line 126
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Binary_eq line 132
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1LittleRat line 152
26. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Little line 157
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Little_sound line 161
28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half line 169
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_0_0 line 185
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_0_1 line 189
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_0_2 line 193
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_0_3 line 197
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_0_4 line 201
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_0_5 line 205
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_1_0 line 209
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_1_1 line 213
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_1_2 line 217
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_1_3 line 221
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_1_4 line 225
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_1_5 line 229
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_2_0 line 233
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_2_1 line 237
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_2_2 line 241
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_2_3 line 245
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_2_4 line 249
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_check_2_5 line 253
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Half_sound line 257
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1D line 292
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1D_sound line 293
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1OneD line 296
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1OneD_sound line 297
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1EDLogWitness line 301
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1EDLog line 302
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1EDLog_sound line 303
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1ED line 307
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1ED_sound line 308
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1EOneDLogWitness line 310
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1EOneDLog line 311
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1EOneDLog_sound line 312
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1EOneD line 316
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1EOneD_sound line 317
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1BinaryEntropy line 319
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1BinaryEntropy_sound line 320
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1Leaf line 324
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1Leaf_sound line 325
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1Mass line 335
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U1_2_1Mass_sound line 336
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1D line 341
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1D_sound line 342
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1OneD line 345
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1OneD_sound line 346
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1EDLogWitness line 350
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1EDLog line 351
74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1EDLog_sound line 352
75. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1ED line 356
76. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1ED_sound line 357
77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1EOneDLogWitness line 359
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1EOneDLog line 360
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1EOneDLog_sound line 361
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1EOneD line 365
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1EOneD_sound line 366
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1BinaryEntropy line 368
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1BinaryEntropy_sound line 369
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1Leaf line 373
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1Leaf_sound line 374
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1Mass line 384
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_1_1Mass_sound line 385
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0D line 390
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0D_sound line 391
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0OneD line 394
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0OneD_sound line 395
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0EDLogWitness line 399
93. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0EDLog line 400
94. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0EDLog_sound line 401
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0ED line 405
96. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0ED_sound line 406
97. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0EOneDLogWitness line 408
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0EOneDLog line 409
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0EOneDLog_sound line 410
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0EOneD line 414
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0EOneD_sound line 415
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0BinaryEntropy line 417
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0BinaryEntropy_sound line 418
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0Leaf line 422
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0Leaf_sound line 423
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0Mass line 431
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U2_2_0Mass_sound line 432
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U3_0_1Leaf line 437
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U3_0_1Leaf_sound line 438
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U3_0_1Mass line 442
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U3_0_1Mass_sound line 443
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U3_1_0Leaf line 448
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U3_1_0Leaf_sound line 449
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U3_1_0Mass line 453
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U3_1_0Mass_sound line 454
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U4_0_0Leaf line 459
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U4_0_0Leaf_sound line 460
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U4_0_0Mass line 464
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1U4_0_0Mass_sound line 465
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Leaves line 470
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Leaves_sound line 479
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Masses line 490
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Masses_sound line 499
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Binaries line 510
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1Binaries_sound line 516
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1S2 line 524
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_2_1S2_sound line 525