OAI/Analysis/Quantum/DimensionTen/TensorKraus.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.DimensionTen.sum_kroneckerline 11 - lemma
OAI.DimensionTen.kronecker_sumline 17 - lemma
OAI.DimensionTen.block_expansionline 23 - lemma
OAI.DimensionTen.sum_four_commline 29 - lemma
OAI.DimensionTen.tensorMap_krausline 38 - lemma
OAI.DimensionTen.krausMap_conjugateline 52 - lemma
OAI.DimensionTen.krausMap_postconjugateline 62 - lemma
OAI.DimensionTen.krausMap_preconjugateline 70