OAI/LinearAlgebra/Hadamard/Equivalence.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Rephasing, permutation equivalence and dephasing.

  1. def OAI.HadamardSix.rephase line 11
  2. lemma OAI.HadamardSix.IsComplexHadamard.rephase line 14
  3. lemma OAI.HadamardSix.IsComplexHadamard.permute_rows line 35
  4. lemma OAI.HadamardSix.IsComplexHadamard.permute_columns line 41
  5. lemma OAI.HadamardSix.HadamardEquivalent.refl line 48
  6. lemma OAI.HadamardSix.HadamardEquivalent.symm line 51
  7. lemma OAI.HadamardSix.HadamardEquivalent.trans line 66
  8. lemma OAI.HadamardSix.HadamardEquivalent.hadamard line 82
  9. def OAI.HadamardSix.dephase line 91
  10. lemma OAI.HadamardSix.dephase_equivalent line 94
  11. lemma OAI.HadamardSix.dephase_first_row line 105
  12. lemma OAI.HadamardSix.dephase_first_column line 113
  13. lemma OAI.HadamardSix.IsComplexHadamard.dephase line 118
  14. lemma OAI.HadamardSix.entrywiseSquare_rephase line 121
  15. lemma OAI.HadamardSix.HadamardEquivalent.entrywiseSquare line 127
  16. lemma OAI.HadamardSix.dephase_square_hadamard line 138
  17. lemma OAI.HadamardSix.permuteCharge_trans line 143
  18. lemma OAI.HadamardSix.g_equivalence_covariance line 146
  19. lemma OAI.HadamardSix.HadamardEquivalent.fourier_vanishing_iff line 159