OAI/LinearAlgebra/MatrixFields/CapacityA/CapA2_6_8I2Pair.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairValue line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairRaw line 17
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairRaw_sound line 18
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairCertificates line 21
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairCertificates_valid line 58
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairCertificateIndex line 60
7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP line 259
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_0_0 line 261
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_0_1 line 263
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_0_2 line 265
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_0_3 line 267
12. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_0_4 line 269
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_0_5 line 271
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_1_0 line 273
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_1_1 line 275
16. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_1_2 line 277
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_1_3 line 279
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_1_4 line 281
19. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_1_5 line 283
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_2_0 line 285
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_2_1 line 287
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_2_2 line 289
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_2_3 line 291
24. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_2_4 line 293
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_2_5 line 295
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_3_0 line 297
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_3_1 line 299
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_3_2 line 301
29. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_3_3 line 303
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_3_4 line 305
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_3_5 line 307
32. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_4_0 line 309
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_4_1 line 311
34. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_4_2 line 313
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_4_3 line 315
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_4_4 line 317
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_4_5 line 319
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_5_0 line 321
39. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_5_1 line 323
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_5_2 line 325
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_5_3 line 327
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_5_4 line 329
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check_5_5 line 331
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_check line 333
45. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairP_sound line 343
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairTerms line 346
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairTerms_sound line 348
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairEntropy line 352
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairEntropy_sound line 353
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairMass line 355
51. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairMass_sound line 356
52. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairMassTermLogWitness line 358
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairMassTermLog line 359
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairMassTermLog_sound line 360
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairMassTerm line 364
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairMassTerm_sound line 365
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairH line 367
58. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA2_6_8I2PairH_sound line 368