OAI/Analysis/MutuallyUnbiased/Tao/TaoArithmetic.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Exact arithmetic in ℤ[ω], interpreted in the same complex root as Tao's matrix. These definitions are for certificate checking, not assumptions.

  1. abbrev OAI.MUB6.TaoArithmetic.Coeff line 14
  2. def OAI.MUB6.TaoArithmetic.value line 16
  3. def OAI.MUB6.TaoArithmetic.mul line 18
  4. def OAI.MUB6.TaoArithmetic.conjugate line 21
  5. def OAI.MUB6.TaoArithmetic.root line 23
  6. theorem OAI.MUB6.TaoArithmetic.value_zero line 26
  7. theorem OAI.MUB6.TaoArithmetic.value_add line 28
  8. theorem OAI.MUB6.TaoArithmetic.value_mul line 32
  9. theorem OAI.MUB6.TaoArithmetic.value_conjugate line 36
  10. theorem OAI.MUB6.TaoArithmetic.value_sum line 41
  11. theorem OAI.MUB6.TaoArithmetic.omega_zpow_mod line 48
  12. theorem OAI.MUB6.TaoArithmetic.value_root line 57
  13. def OAI.MUB6.TaoArithmetic.counts line 69
  14. theorem OAI.MUB6.TaoArithmetic.omega_zpow_sum line 72
  15. theorem OAI.MUB6.TaoArithmetic.counts_interpretation line 81