OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row10.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_0 line 13
  2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_0 line 15
  3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_0 line 19
  4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_0 line 38
  5. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_1 line 45
  6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_1 line 47
  7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_1 line 51
  8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_1 line 70
  9. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_2 line 77
  10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_2 line 79
  11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_2 line 83
  12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_2 line 102
  13. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_3 line 109
  14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_3 line 111
  15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_3 line 115
  16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_3 line 134
  17. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_4 line 141
  18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_4 line 143
  19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_4 line 147
  20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_4 line 166
  21. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_5 line 173
  22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_5 line 175
  23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_5 line 179
  24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_5 line 198
  25. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_6 line 205
  26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_6 line 207
  27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_6 line 211
  28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_6 line 230
  29. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_7 line 237
  30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_7 line 239
  31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_7 line 243
  32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_7 line 262
  33. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_8 line 269
  34. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_8 line 271
  35. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_8 line 275
  36. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_8 line 294
  37. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_9 line 301
  38. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_9 line 303
  39. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_9 line 307
  40. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_9 line 326
  41. def OAI.MUB6.Certificate.GramEntries.Block1.rows10_10 line 333
  42. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck10_10 line 335
  43. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound10_10 line 339
  44. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval10_10 line 358