OAI/Analysis/MutuallyUnbiased/Matrix/Equivalence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.phaseTransform line 10
  2. theorem OAI.MUB6.IsHadamard.phaseTransform line 13
  3. theorem OAI.MUB6.IsHadamard.permutations line 43
  4. theorem OAI.MUB6.Equivalent.isHadamard line 53
  5. def OAI.MUB6.dephase line 62
  6. theorem OAI.MUB6.dephase_equivalent line 65
  7. theorem OAI.MUB6.dephase_isHadamard line 76
  8. theorem OAI.MUB6.dephase_row_zero line 79
  9. theorem OAI.MUB6.dephase_column_zero line 84
  10. theorem OAI.MUB6.equivalent_squares line 89
  11. theorem OAI.MUB6.dephase_square_isHadamard line 102