OAI/LinearAlgebra/MatrixFields/Certificates/LittleB1_3_4.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.shapes4_list line 15
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Binary line 31
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Binary_eq line 35
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6LittleRat line 55
5. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Little line 60
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Little_sound line 64
7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half line 72
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_0_0 line 84
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_0_1 line 88
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_0_2 line 92
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_0_3 line 96
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_0_4 line 100
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_0_5 line 104
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_1_0 line 108
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_1_1 line 112
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_1_2 line 116
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_1_3 line 120
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_1_4 line 124
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_1_5 line 128
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_2_0 line 132
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_2_1 line 136
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_2_2 line 140
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_2_3 line 144
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_2_4 line 148
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_check_2_5 line 152
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_1_6Half_sound line 156
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5_below line 180
28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Raw line 187
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Raw_0_0_4 line 196
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Raw_0_1_3 line 200
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Raw_0_2_2 line 204
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Raw_1_0_3 line 208
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Raw_1_1_2 line 212
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Raw_1_2_1 line 216
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Raw_sound line 220
36. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Den line 231
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Den_sound line 232
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Den_positive line 234
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Table line 235
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Law line 244
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Law_check_0_0_4 line 245
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Law_check_0_1_3 line 246
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Law_check_0_2_2 line 247
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Law_check_1_0_3 line 248
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Law_check_1_1_2 line 249
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Law_check_1_2_1 line 250
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Law_check line 251
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Law_sound line 262
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Binary line 278
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Binary_eq line 283
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5LittleRat line 303
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Little line 308
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Little_sound line 312
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half line 320
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_0_0 line 336
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_0_1 line 340
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_0_2 line 344
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_0_3 line 348
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_0_4 line 352
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_0_5 line 356
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_1_0 line 360
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_1_1 line 364
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_1_2 line 368
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_1_3 line 372
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_1_4 line 376
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_1_5 line 380
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_2_0 line 384
68. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_2_1 line 388
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_2_2 line 392
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_2_3 line 396
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_2_4 line 400
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_check_2_5 line 404
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_2_5Half_sound line 408
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Binary line 426
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Binary_eq line 432
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4LittleRat line 452
77. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Little line 457
78. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Little_sound line 461
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half line 469
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_0_0 line 488
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_0_1 line 492
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_0_2 line 496
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_0_3 line 500
84. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_0_4 line 504
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_0_5 line 508
86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_1_0 line 512
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_1_1 line 516
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_1_2 line 520
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_1_3 line 524
90. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_1_4 line 528
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_1_5 line 532
92. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_2_0 line 536
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_2_1 line 540
94. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_2_2 line 544
95. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_2_3 line 548
96. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_2_4 line 552
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_check_2_5 line 556
98. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_3_4Half_sound line 560