OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row14.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_0 line 14
  2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_0 line 16
  3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_0 line 20
  4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_0 line 33
  5. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_1 line 40
  6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_1 line 42
  7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_1 line 46
  8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_1 line 59
  9. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_2 line 66
  10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_2 line 68
  11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_2 line 72
  12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_2 line 85
  13. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_3 line 92
  14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_3 line 94
  15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_3 line 98
  16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_3 line 111
  17. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_4 line 118
  18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_4 line 120
  19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_4 line 124
  20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_4 line 137
  21. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_5 line 144
  22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_5 line 146
  23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_5 line 150
  24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_5 line 163
  25. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_6 line 170
  26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_6 line 172
  27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_6 line 176
  28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_6 line 189
  29. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_7 line 196
  30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_7 line 198
  31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_7 line 202
  32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_7 line 215
  33. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_8 line 222
  34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_8 line 224
  35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_8 line 228
  36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_8 line 241
  37. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_9 line 248
  38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_9 line 250
  39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_9 line 254
  40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_9 line 267
  41. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_10 line 274
  42. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_10 line 276
  43. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_10 line 280
  44. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_10 line 293
  45. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_11 line 300
  46. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_11 line 302
  47. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_11 line 306
  48. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_11 line 319
  49. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_12 line 326
  50. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_12 line 328
  51. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_12 line 332
  52. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_12 line 345
  53. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_13 line 352
  54. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_13 line 354
  55. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_13 line 358
  56. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_13 line 371
  57. def OAI.MUB6.Certificate.GramEntries.Block3.rows14_14 line 378
  58. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck14_14 line 380
  59. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound14_14 line 384
  60. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval14_14 line 397