OAI/LinearAlgebra/MatrixFields/Certificates/SplitA2_7_7.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7_below line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw line 39
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_0_1_7 line 64
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_0_2_6 line 68
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_0_3_5 line 72
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_0_4_4 line 76
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_0_5_3 line 80
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_0_6_2 line 84
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_0_7_1 line 88
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_1_0_7 line 92
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_1_1_6 line 96
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_1_2_5 line 100
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_1_3_4 line 104
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_1_4_3 line 108
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_1_5_2 line 112
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_1_6_1 line 116
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_1_7_0 line 120
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_2_0_6 line 124
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_2_1_5 line 128
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_2_2_4 line 132
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_2_3_3 line 136
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_2_4_2 line 140
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_2_5_1 line 144
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_2_6_0 line 148
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Raw_sound line 152
26. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Den line 179
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Den_sound line 180
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Den_positive line 182
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Table line 183
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law line 208
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_0_1_7 line 209
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_0_2_6 line 210
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_0_3_5 line 211
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_0_4_4 line 212
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_0_5_3 line 213
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_0_6_2 line 214
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_0_7_1 line 215
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_1_0_7 line 216
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_1_1_6 line 217
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_1_2_5 line 218
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_1_3_4 line 219
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_1_4_3 line 220
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_1_5_2 line 221
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_1_6_1 line 222
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_1_7_0 line 223
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_2_0_6 line 224
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_2_1_5 line 225
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_2_2_4 line 226
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_2_3_3 line 227
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_2_4_2 line 228
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_2_5_1 line 229
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check_2_6_0 line 230
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_check line 231
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.A2_7_7Law_sound line 258