OAI/Analysis/MutuallyUnbiased/GramEntries/Block4Row14.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_0 line 19
  2. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_0 line 21
  3. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_0 line 25
  4. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_0 line 66
  5. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_1 line 73
  6. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_1 line 75
  7. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_1 line 79
  8. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_1 line 120
  9. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_2 line 127
  10. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_2 line 129
  11. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_2 line 133
  12. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_2 line 174
  13. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_3 line 181
  14. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_3 line 183
  15. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_3 line 187
  16. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_3 line 228
  17. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_4 line 235
  18. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_4 line 237
  19. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_4 line 241
  20. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_4 line 282
  21. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_5 line 289
  22. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_5 line 291
  23. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_5 line 295
  24. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_5 line 336
  25. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_6 line 343
  26. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_6 line 345
  27. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_6 line 349
  28. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_6 line 390
  29. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_7 line 397
  30. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_7 line 399
  31. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_7 line 403
  32. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_7 line 444
  33. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_8 line 451
  34. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_8 line 453
  35. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_8 line 457
  36. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_8 line 498
  37. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_9 line 505
  38. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_9 line 507
  39. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_9 line 511
  40. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_9 line 552
  41. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_10 line 559
  42. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_10 line 561
  43. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_10 line 565
  44. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_10 line 606
  45. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_11 line 613
  46. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_11 line 615
  47. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_11 line 619
  48. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_11 line 660
  49. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_12 line 667
  50. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_12 line 669
  51. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_12 line 673
  52. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_12 line 714
  53. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_13 line 721
  54. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_13 line 723
  55. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_13 line 727
  56. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_13 line 768
  57. def OAI.MUB6.Certificate.GramEntries.Block4.rows14_14 line 775
  58. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck14_14 line 777
  59. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound14_14 line 781
  60. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval14_14 line 822