OAI/LinearAlgebra/MatrixFields/Certificates/SupportedContraction.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Binary line 20
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Binary_eq line 29
3. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3LittleRat line 49
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Little line 54
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Little_sound line 58
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half line 66
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_0_0 line 86
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_0_1 line 90
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_0_2 line 94
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_0_3 line 98
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_0_4 line 102
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_0_5 line 106
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_1_0 line 110
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_1_1 line 114
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_1_2 line 118
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_1_3 line 122
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_1_4 line 126
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_1_5 line 130
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_2_0 line 134
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_2_1 line 138
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_2_2 line 142
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_2_3 line 146
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_2_4 line 150
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_check_2_5 line 154
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B3_2_3Half_sound line 158
26. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Binary line 193
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Binary_eq line 199
28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2LittleRat line 219
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Little line 224
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Little_sound line 228
31. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half line 236
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_0_0 line 252
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_0_1 line 256
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_0_2 line 260
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_0_3 line 264
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_0_4 line 268
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_0_5 line 272
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_1_0 line 276
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_1_1 line 280
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_1_2 line 284
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_1_3 line 288
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_1_4 line 292
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_1_5 line 296
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_2_0 line 300
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_2_1 line 304
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_2_2 line 308
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_2_3 line 312
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_2_4 line 316
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_check_2_5 line 320
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.B5_1_2Half_sound line 324
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.halfTable line 359
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.halfTable_sound line 407
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.halfProbs line 457
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.halfProbs_sound line 459
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.pairDegree line 484
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.halfTable_degree_zero_0 line 486
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.halfTable_degree_zero_1 line 489
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.halfTable_degree_zero_2 line 492
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.halfTable_degree_zero line 496
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.listSumBall_eq_zero line 503
61. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.stageAPairBall_zero line 512
62. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.stageAPairBall line 530
63. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.stageAPairBall_eq line 536
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.stageAPairBall_sound line 545