OAI/InformationTheory/AmplitudeDamping/TensorEntropy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GAD.diagonalStarAlgHom line 27
  2. theorem OAI.GAD.entropy_diagonal line 32
  3. def OAI.GAD.reindexStarAlgEquiv line 55
  4. theorem OAI.GAD.trace_reindex line 61
  5. theorem OAI.GAD.entropy_reindex line 65
  6. def OAI.GAD.tensorUnitary line 86
  7. theorem OAI.GAD.entropy_kronecker line 90
  8. theorem OAI.GAD.entropy_kronecker_state line 117