OAI/LinearAlgebra/MatrixFields/CapacityA/CapA1_6_9I1Pair.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairValue line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairRaw line 17
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairRaw_sound line 18
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairCertificates line 21
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairCertificates_valid line 50
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairCertificateIndex line 52
7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP line 205
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_0_0 line 207
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_0_1 line 209
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_0_2 line 211
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_0_3 line 213
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_0_4 line 215
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_0_5 line 217
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_1_0 line 219
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_1_1 line 221
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_1_2 line 223
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_1_3 line 225
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_1_4 line 227
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_1_5 line 229
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_2_0 line 231
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_2_1 line 233
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_2_2 line 235
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_2_3 line 237
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_2_4 line 239
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_2_5 line 241
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_3_0 line 243
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_3_1 line 245
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_3_2 line 247
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_3_3 line 249
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_3_4 line 251
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_3_5 line 253
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_4_0 line 255
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_4_1 line 257
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_4_2 line 259
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_4_3 line 261
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_4_4 line 263
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_4_5 line 265
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_5_0 line 267
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_5_1 line 269
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_5_2 line 271
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_5_3 line 273
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_5_4 line 275
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check_5_5 line 277
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_check line 279
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairP_sound line 289
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairTerms line 292
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairTerms_sound line 294
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairEntropy line 298
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairEntropy_sound line 299
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairMass line 301
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairMass_sound line 302
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairMassTermLogWitness line 304
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairMassTermLog line 305
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairMassTermLog_sound line 306
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairMassTerm line 310
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairMassTerm_sound line 311
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairH line 313
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA1_6_9I1PairH_sound line 314