OAI/LinearAlgebra/MatrixFields/Certificates/SplitA3_6_7.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw line 43
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_0_1_7 line 72
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_0_2_6 line 76
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_0_3_5 line 80
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_0_4_4 line 84
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_0_5_3 line 88
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_0_6_2 line 92
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_1_0_7 line 96
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_1_1_6 line 100
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_1_2_5 line 104
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_1_3_4 line 108
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_1_4_3 line 112
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_1_5_2 line 116
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_1_6_1 line 120
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_2_0_6 line 124
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_2_1_5 line 128
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_2_2_4 line 132
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_2_3_3 line 136
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_2_4_2 line 140
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_2_5_1 line 144
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_2_6_0 line 148
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_3_0_5 line 152
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_3_1_4 line 156
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_3_2_3 line 160
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_3_3_2 line 164
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_3_4_1 line 168
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_3_5_0 line 172
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Raw_sound line 176
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Den line 207
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Den_sound line 208
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Den_positive line 210
33. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Table line 211
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law line 240
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_0_1_7 line 241
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_0_2_6 line 242
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_0_3_5 line 243
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_0_4_4 line 244
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_0_5_3 line 245
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_0_6_2 line 246
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_1_0_7 line 247
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_1_1_6 line 248
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_1_2_5 line 249
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_1_3_4 line 250
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_1_4_3 line 251
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_1_5_2 line 252
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_1_6_1 line 253
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_2_0_6 line 254
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_2_1_5 line 255
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_2_2_4 line 256
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_2_3_3 line 257
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_2_4_2 line 258
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_2_5_1 line 259
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_2_6_0 line 260
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_3_0_5 line 261
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_3_1_4 line 262
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_3_2_3 line 263
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_3_3_2 line 264
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_3_4_1 line 265
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check_3_5_0 line 266
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_check line 267
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A3_6_7Law_sound line 298