OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row9.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_0 line 16
  2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_0 line 18
  3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_0 line 22
  4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_0 line 63
  5. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_1 line 70
  6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_1 line 72
  7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_1 line 76
  8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_1 line 117
  9. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_2 line 124
  10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_2 line 126
  11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_2 line 130
  12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_2 line 171
  13. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_3 line 178
  14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_3 line 180
  15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_3 line 184
  16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_3 line 225
  17. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_4 line 232
  18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_4 line 234
  19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_4 line 238
  20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_4 line 279
  21. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_5 line 286
  22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_5 line 288
  23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_5 line 292
  24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_5 line 333
  25. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_6 line 340
  26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_6 line 342
  27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_6 line 346
  28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_6 line 387
  29. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_7 line 394
  30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_7 line 396
  31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_7 line 400
  32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_7 line 441
  33. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_8 line 448
  34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_8 line 450
  35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_8 line 454
  36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_8 line 495
  37. def OAI.MUB6.Certificate.GramEntries.Block3.rows9_9 line 502
  38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck9_9 line 504
  39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound9_9 line 508
  40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval9_9 line 549