OAI/LinearAlgebra/MatrixFields/Certificates/SplitA4_5_7.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw line 45
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_0_1_7 line 76
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_0_2_6 line 80
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_0_3_5 line 84
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_0_4_4 line 88
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_0_5_3 line 92
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_1_0_7 line 96
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_1_1_6 line 100
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_1_2_5 line 104
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_1_3_4 line 108
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_1_4_3 line 112
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_1_5_2 line 116
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_2_0_6 line 120
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_2_1_5 line 124
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_2_2_4 line 128
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_2_3_3 line 132
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_2_4_2 line 136
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_2_5_1 line 140
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_3_0_5 line 144
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_3_1_4 line 148
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_3_2_3 line 152
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_3_3_2 line 156
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_3_4_1 line 160
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_3_5_0 line 164
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_4_0_4 line 168
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_4_1_3 line 172
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_4_2_2 line 176
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_4_3_1 line 180
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_4_4_0 line 184
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Raw_sound line 188
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Den line 221
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Den_sound line 222
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Den_positive line 224
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Table line 225
36. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law line 256
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_0_1_7 line 257
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_0_2_6 line 258
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_0_3_5 line 259
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_0_4_4 line 260
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_0_5_3 line 261
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_1_0_7 line 262
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_1_1_6 line 263
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_1_2_5 line 264
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_1_3_4 line 265
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_1_4_3 line 266
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_1_5_2 line 267
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_2_0_6 line 268
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_2_1_5 line 269
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_2_2_4 line 270
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_2_3_3 line 271
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_2_4_2 line 272
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_2_5_1 line 273
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_3_0_5 line 274
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_3_1_4 line 275
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_3_2_3 line 276
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_3_3_2 line 277
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_3_4_1 line 278
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_3_5_0 line 279
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_4_0_4 line 280
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_4_1_3 line 281
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_4_2_2 line 282
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_4_3_1 line 283
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check_4_4_0 line 284
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_check line 285
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A4_5_7Law_sound line 318