OAI/LinearAlgebra/MatrixFields/Certificates/SplitA3_5_8.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw line 41
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_0_0_8 line 68
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_0_1_7 line 72
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_0_2_6 line 76
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_0_3_5 line 80
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_0_4_4 line 84
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_0_5_3 line 88
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_1_0_7 line 92
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_1_1_6 line 96
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_1_2_5 line 100
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_1_3_4 line 104
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_1_4_3 line 108
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_1_5_2 line 112
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_2_0_6 line 116
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_2_1_5 line 120
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_2_2_4 line 124
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_2_3_3 line 128
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_2_4_2 line 132
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_2_5_1 line 136
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_3_0_5 line 140
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_3_1_4 line 144
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_3_2_3 line 148
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_3_3_2 line 152
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_3_4_1 line 156
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_3_5_0 line 160
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Raw_sound line 164
28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Den line 193
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Den_sound line 194
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Den_positive line 196
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Table line 197
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law line 224
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_0_0_8 line 225
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_0_1_7 line 226
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_0_2_6 line 227
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_0_3_5 line 228
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_0_4_4 line 229
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_0_5_3 line 230
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_1_0_7 line 231
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_1_1_6 line 232
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_1_2_5 line 233
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_1_3_4 line 234
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_1_4_3 line 235
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_1_5_2 line 236
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_2_0_6 line 237
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_2_1_5 line 238
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_2_2_4 line 239
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_2_3_3 line 240
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_2_4_2 line 241
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_2_5_1 line 242
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_3_0_5 line 243
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_3_1_4 line 244
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_3_2_3 line 245
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_3_3_2 line 246
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_3_4_1 line 247
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check_3_5_0 line 248
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_check line 249
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_5_8Law_sound line 278