OAI/Analysis/MutuallyUnbiased/Tao/Tao.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The explicit five-cycle representative of Tao's cubic matrix.

  1. theorem OAI.MUB6.omega_isPrimitiveRoot line 15
  2. theorem OAI.MUB6.omega_cube line 18
  3. theorem OAI.MUB6.omega_norm line 20
  4. theorem OAI.MUB6.omega_normSq line 23
  5. theorem OAI.MUB6.omega_sum line 27
  6. theorem OAI.MUB6.omega_conj line 31
  7. theorem OAI.MUB6.omega_four line 40
  8. theorem OAI.MUB6.omega_five line 45
  9. theorem OAI.MUB6.omega_six line 50
  10. theorem OAI.MUB6.tao_entries_unit line 55
  11. theorem OAI.MUB6.tao_gram line 58
  12. theorem OAI.MUB6.tao_isHadamard line 67
  13. theorem OAI.MUB6.isHadamard_conj line 69
  14. theorem OAI.MUB6.tao_square_eq_conj line 82
  15. theorem OAI.MUB6.tao_square_isHadamard line 87