OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row14.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_0 line 15
  2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_0 line 17
  3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_0 line 21
  4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_0 line 50
  5. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_1 line 57
  6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_1 line 59
  7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_1 line 63
  8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_1 line 92
  9. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_2 line 99
  10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_2 line 101
  11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_2 line 105
  12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_2 line 134
  13. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_3 line 141
  14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_3 line 143
  15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_3 line 147
  16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_3 line 176
  17. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_4 line 183
  18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_4 line 185
  19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_4 line 189
  20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_4 line 218
  21. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_5 line 225
  22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_5 line 227
  23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_5 line 231
  24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_5 line 260
  25. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_6 line 267
  26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_6 line 269
  27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_6 line 273
  28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_6 line 302
  29. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_7 line 309
  30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_7 line 311
  31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_7 line 315
  32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_7 line 344
  33. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_8 line 351
  34. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_8 line 353
  35. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_8 line 357
  36. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_8 line 386
  37. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_9 line 393
  38. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_9 line 395
  39. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_9 line 399
  40. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_9 line 428
  41. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_10 line 435
  42. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_10 line 437
  43. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_10 line 441
  44. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_10 line 470
  45. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_11 line 477
  46. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_11 line 479
  47. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_11 line 483
  48. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_11 line 512
  49. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_12 line 519
  50. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_12 line 521
  51. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_12 line 525
  52. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_12 line 554
  53. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_13 line 561
  54. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_13 line 563
  55. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_13 line 567
  56. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_13 line 596
  57. def OAI.MUB6.Certificate.GramEntries.Block1.rows14_14 line 603
  58. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck14_14 line 605
  59. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound14_14 line 609
  60. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval14_14 line 638