OAI/LinearAlgebra/MatrixFields/Certificates/Terminal1_6_1.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1_below line 17
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Raw line 22
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Raw_0_3_1 line 29
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Raw_0_4_0 line 33
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Raw_1_2_1 line 37
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Raw_1_3_0 line 41
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Raw_sound line 45
8. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Den line 54
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Den_sound line 55
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Den_positive line 57
11. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Table line 58
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Law line 65
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Law_check_0_3_1 line 66
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Law_check_0_4_0 line 67
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Law_check_1_2_1 line 68
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Law_check_1_3_0 line 69
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Law_check line 70
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Law_sound line 79
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Binary line 106
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Binary_eq line 110
21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1LittleRat line 130
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Little line 135
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Little_sound line 139
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half line 147
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_0_0 line 159
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_0_1 line 163
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_0_2 line 167
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_0_3 line 171
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_0_4 line 175
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_0_5 line 179
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_1_0 line 183
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_1_1 line 187
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_1_2 line 191
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_1_3 line 195
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_1_4 line 199
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_1_5 line 203
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_2_0 line 207
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_2_1 line 211
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_2_2 line 215
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_2_3 line 219
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_2_4 line 223
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_check_2_5 line 227
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Half_sound line 231
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U0_3_1Leaf line 266
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U0_3_1Leaf_sound line 267
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U0_3_1Mass line 271
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U0_3_1Mass_sound line 272
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U0_4_0Leaf line 277
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U0_4_0Leaf_sound line 278
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U0_4_0Mass line 282
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U0_4_0Mass_sound line 283
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1D line 288
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1D_sound line 289
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1OneD line 292
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1OneD_sound line 293
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1EDLogWitness line 297
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1EDLog line 298
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1EDLog_sound line 299
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1ED line 303
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1ED_sound line 304
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1EOneDLogWitness line 306
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1EOneDLog line 307
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1EOneDLog_sound line 308
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1EOneD line 312
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1EOneD_sound line 313
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1BinaryEntropy line 315
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1BinaryEntropy_sound line 316
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1Leaf line 320
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1Leaf_sound line 321
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1Mass line 332
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_2_1Mass_sound line 333
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_3_0Leaf line 338
73. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_3_0Leaf_sound line 339
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_3_0Mass line 343
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1U1_3_0Mass_sound line 344
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Leaves line 349
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Leaves_sound line 356
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Masses line 365
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Masses_sound line 372
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Binaries line 381
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1Binaries_sound line 385
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1S2 line 392
83. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B1_6_1S2_sound line 393