OAI/Analysis/MutuallyUnbiased/GramData/Block3Data.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Exact integer matrix for λ = (1, 4), m = 27, exponent = 14.

  1. def OAI.MUB6.Certificate.GramData.Block3.Z line 14
  2. def OAI.MUB6.Certificate.GramData.Block3.entries line 44
  3. def OAI.MUB6.Certificate.GramData.Block3.D line 74
  4. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_0 line 76
  5. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_1 line 78
  6. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_2 line 80
  7. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_3 line 82
  8. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_4 line 84
  9. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_5 line 86
  10. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_6 line 88
  11. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_7 line 90
  12. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_8 line 92
  13. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_9 line 94
  14. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_10 line 96
  15. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_11 line 98
  16. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_12 line 100
  17. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_13 line 102
  18. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_14 line 104
  19. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_15 line 106
  20. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_16 line 108
  21. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_17 line 110
  22. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_18 line 112
  23. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_19 line 114
  24. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_20 line 116
  25. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_21 line 118
  26. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_22 line 120
  27. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_23 line 122
  28. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_24 line 124
  29. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_25 line 126
  30. theorem OAI.MUB6.Certificate.GramData.Block3.pivot_26 line 128