OAI/Analysis/MutuallyUnbiased/Bases/Tensor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Explicit mutually unbiased bases from two- and three-dimensional unitary matrices.

  1. abbrev OAI.MUB6.ThreeTensor.MatrixTwo line 14
  2. abbrev OAI.MUB6.ThreeTensor.MatrixThree line 15
  3. def OAI.MUB6.ThreeTensor.coordEquiv line 17
  4. def OAI.MUB6.ThreeTensor.tensorMatrix line 19
  5. lemma OAI.MUB6.ThreeTensor.tensor_cross line 23
  6. lemma OAI.MUB6.ThreeTensor.tensor_gram line 40
  7. def OAI.MUB6.ThreeTensor.columns line 56
  8. lemma OAI.MUB6.ThreeTensor.columns_inner line 59
  9. lemma OAI.MUB6.ThreeTensor.columns_orthonormal line 64
  10. def OAI.MUB6.ThreeTensor.matrixBasis line 71
  11. lemma OAI.MUB6.ThreeTensor.matrixBasis_apply line 76
  12. theorem OAI.MUB6.ThreeTensor.attainable_three_of_small_matrices line 80