OAI/Analysis/MutuallyUnbiased/GramAssembly/Block0Data.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_0_0 line 11
  2. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_0_1 line 13
  3. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_0_2 line 15
  4. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_0_3 line 17
  5. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_0_4 line 19
  6. def OAI.MUB6.Certificate.GramAssembly.Block0.entryRow0 line 21
  7. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_1_0 line 23
  8. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_1_1 line 25
  9. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_1_2 line 27
  10. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_1_3 line 29
  11. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_1_4 line 31
  12. def OAI.MUB6.Certificate.GramAssembly.Block0.entryRow1 line 33
  13. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_2_0 line 35
  14. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_2_1 line 37
  15. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_2_2 line 39
  16. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_2_3 line 41
  17. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_2_4 line 43
  18. def OAI.MUB6.Certificate.GramAssembly.Block0.entryRow2 line 45
  19. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_3_0 line 47
  20. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_3_1 line 49
  21. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_3_2 line 51
  22. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_3_3 line 53
  23. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_3_4 line 55
  24. def OAI.MUB6.Certificate.GramAssembly.Block0.entryRow3 line 57
  25. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_4_0 line 59
  26. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_4_1 line 61
  27. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_4_2 line 63
  28. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_4_3 line 65
  29. def OAI.MUB6.Certificate.GramAssembly.Block0.entry_4_4 line 67
  30. def OAI.MUB6.Certificate.GramAssembly.Block0.entryRow4 line 69
  31. def OAI.MUB6.Certificate.GramAssembly.Block0.entryRows line 71
  32. def OAI.MUB6.Certificate.GramAssembly.Block0.entries line 73
  33. def OAI.MUB6.Certificate.GramAssembly.Block0.weights line 76
  34. theorem OAI.MUB6.Certificate.GramAssembly.Block0.weights_cast_0 line 84
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block0.weights_cast_1 line 89
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block0.weights_cast_2 line 94
  37. theorem OAI.MUB6.Certificate.GramAssembly.Block0.weights_cast_3 line 99
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block0.weights_cast_4 line 104
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block0.weights_cast line 109