OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row13.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_0 line 13
  2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_0 line 15
  3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_0 line 19
  4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_0 line 38
  5. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_1 line 45
  6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_1 line 47
  7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_1 line 51
  8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_1 line 70
  9. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_2 line 77
  10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_2 line 79
  11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_2 line 83
  12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_2 line 102
  13. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_3 line 109
  14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_3 line 111
  15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_3 line 115
  16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_3 line 134
  17. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_4 line 141
  18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_4 line 143
  19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_4 line 147
  20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_4 line 166
  21. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_5 line 173
  22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_5 line 175
  23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_5 line 179
  24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_5 line 198
  25. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_6 line 205
  26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_6 line 207
  27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_6 line 211
  28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_6 line 230
  29. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_7 line 237
  30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_7 line 239
  31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_7 line 243
  32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_7 line 262
  33. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_8 line 269
  34. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_8 line 271
  35. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_8 line 275
  36. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_8 line 294
  37. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_9 line 301
  38. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_9 line 303
  39. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_9 line 307
  40. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_9 line 326
  41. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_10 line 333
  42. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_10 line 335
  43. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_10 line 339
  44. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_10 line 358
  45. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_11 line 365
  46. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_11 line 367
  47. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_11 line 371
  48. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_11 line 390
  49. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_12 line 397
  50. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_12 line 399
  51. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_12 line 403
  52. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_12 line 422
  53. def OAI.MUB6.Certificate.GramEntries.Block1.rows13_13 line 429
  54. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck13_13 line 431
  55. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound13_13 line 435
  56. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval13_13 line 454