OAI/LinearAlgebra/MatrixFields/Certificates/Terminal2_1_5.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Raw line 24
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Raw_0_0_4 line 33
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Raw_0_1_3 line 37
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Raw_1_0_3 line 41
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Raw_1_1_2 line 45
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Raw_2_0_2 line 49
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Raw_2_1_1 line 53
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Raw_sound line 57
10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Den line 68
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Den_sound line 69
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Den_positive line 71
13. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Table line 72
14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Law line 81
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Law_check_0_0_4 line 82
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Law_check_0_1_3 line 83
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Law_check_1_0_3 line 84
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Law_check_1_1_2 line 85
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Law_check_2_0_2 line 86
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Law_check_2_1_1 line 87
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Law_check line 88
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Law_sound line 99
23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Binary line 126
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Binary_eq line 132
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5LittleRat line 152
26. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Little line 157
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Little_sound line 161
28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half line 169
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_0_0 line 185
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_0_1 line 189
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_0_2 line 193
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_0_3 line 197
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_0_4 line 201
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_0_5 line 205
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_1_0 line 209
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_1_1 line 213
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_1_2 line 217
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_1_3 line 221
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_1_4 line 225
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_1_5 line 229
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_2_0 line 233
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_2_1 line 237
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_2_2 line 241
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_2_3 line 245
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_2_4 line 249
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_check_2_5 line 253
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Half_sound line 257
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U0_0_4Leaf line 292
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U0_0_4Leaf_sound line 293
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U0_0_4Mass line 297
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U0_0_4Mass_sound line 298
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U0_1_3Leaf line 303
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U0_1_3Leaf_sound line 304
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U0_1_3Mass line 308
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U0_1_3Mass_sound line 309
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_0_3Leaf line 314
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_0_3Leaf_sound line 315
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_0_3Mass line 319
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_0_3Mass_sound line 320
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2D line 325
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2D_sound line 326
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2OneD line 329
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2OneD_sound line 330
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2EDLogWitness line 334
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2EDLog line 335
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2EDLog_sound line 336
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2ED line 340
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2ED_sound line 341
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2EOneDLogWitness line 343
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2EOneDLog line 344
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2EOneDLog_sound line 345
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2EOneD line 349
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2EOneD_sound line 350
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2BinaryEntropy line 352
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2BinaryEntropy_sound line 353
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2Leaf line 357
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2Leaf_sound line 358
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2Mass line 368
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U1_1_2Mass_sound line 369
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2D line 374
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2D_sound line 375
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2OneD line 378
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2OneD_sound line 379
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2EDLogWitness line 383
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2EDLog line 384
86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2EDLog_sound line 385
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2ED line 389
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2ED_sound line 390
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2EOneDLogWitness line 392
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2EOneDLog line 393
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2EOneDLog_sound line 394
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2EOneD line 398
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2EOneD_sound line 399
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2BinaryEntropy line 401
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2BinaryEntropy_sound line 402
96. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2Leaf line 406
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2Leaf_sound line 407
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2Mass line 415
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_0_2Mass_sound line 416
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1D line 421
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1D_sound line 422
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1OneD line 425
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1OneD_sound line 426
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1EDLogWitness line 430
105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1EDLog line 431
106. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1EDLog_sound line 432
107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1ED line 436
108. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1ED_sound line 437
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1EOneDLogWitness line 439
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1EOneDLog line 440
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1EOneDLog_sound line 441
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1EOneD line 445
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1EOneD_sound line 446
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1BinaryEntropy line 448
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1BinaryEntropy_sound line 449
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1Leaf line 453
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1Leaf_sound line 454
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1Mass line 464
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5U2_1_1Mass_sound line 465
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Leaves line 470
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Leaves_sound line 479
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Masses line 490
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Masses_sound line 499
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Binaries line 510
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5Binaries_sound line 516
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5S2 line 524
127. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B2_1_5S2_sound line 525