OAI/LinearAlgebra/MatrixFields/CapacityA/CapA2_7_7I1Pair.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairValue line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairRaw line 17
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairRaw_sound line 18
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairCertificates line 21
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairCertificates_valid line 51
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairCertificateIndex line 53
7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP line 236
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_0_0 line 238
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_0_1 line 240
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_0_2 line 242
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_0_3 line 244
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_0_4 line 246
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_0_5 line 248
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_1_0 line 250
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_1_1 line 252
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_1_2 line 254
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_1_3 line 256
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_1_4 line 258
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_1_5 line 260
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_2_0 line 262
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_2_1 line 264
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_2_2 line 266
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_2_3 line 268
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_2_4 line 270
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_2_5 line 272
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_3_0 line 274
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_3_1 line 276
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_3_2 line 278
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_3_3 line 280
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_3_4 line 282
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_3_5 line 284
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_4_0 line 286
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_4_1 line 288
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_4_2 line 290
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_4_3 line 292
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_4_4 line 294
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_4_5 line 296
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_5_0 line 298
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_5_1 line 300
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_5_2 line 302
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_5_3 line 304
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_5_4 line 306
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check_5_5 line 308
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_check line 310
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairP_sound line 320
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairTerms line 323
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairTerms_sound line 325
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairEntropy line 329
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairEntropy_sound line 330
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairMass line 332
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairMass_sound line 333
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairMassTermLogWitness line 335
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairMassTermLog line 336
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairMassTermLog_sound line 337
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairMassTerm line 341
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairMassTerm_sound line 342
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairH line 344
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_7_7I1PairH_sound line 345