OAI/LinearAlgebra/Hadamard/TaoExponents.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Cubic exponent symmetries of Tao’s order-six complex Hadamard matrix.

  1. abbrev OAI.HadamardSix.TaoSymmetry.I line 13
  2. abbrev OAI.HadamardSix.TaoSymmetry.Exponents line 14
  3. def OAI.HadamardSix.TaoSymmetry.exponent line 16
  4. def OAI.HadamardSix.TaoSymmetry.RowSymmetry line 19
  5. theorem OAI.HadamardSix.TaoSymmetry.rowSymmetry_one line 23
  6. theorem OAI.HadamardSix.TaoSymmetry.rowSymmetry_mul line 28
  7. def OAI.HadamardSix.TaoSymmetry.symmetryMonoid line 45
  8. def OAI.HadamardSix.TaoSymmetry.columnMap line 50
  9. theorem OAI.HadamardSix.TaoSymmetry.columnMap_bijective line 57
  10. def OAI.HadamardSix.TaoSymmetry.columnPerm line 61
  11. def OAI.HadamardSix.TaoSymmetry.rowPhase line 64
  12. def OAI.HadamardSix.TaoSymmetry.columnPhase line 71
  13. theorem OAI.HadamardSix.TaoSymmetry.adjacent_certificate line 78
  14. theorem OAI.HadamardSix.TaoSymmetry.adjacent_symmetry line 84
  15. theorem OAI.HadamardSix.TaoSymmetry.every_row_permutation line 92