OAI/InformationTheory/Entanglement/TensorTools.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecretKey.single_product line 14
  2. lemma OAI.SecretKey.linearMap_eq_of_tensors line 19
  3. lemma OAI.SecretKey.tensorMap_comp line 32
  4. lemma OAI.SecretKey.tensorMap_ad line 39
  5. lemma OAI.SecretKey.tensorMap_id line 45
  6. lemma OAI.SecretKey.tensorMap_transpose line 51
  7. lemma OAI.SecretKey.cp_tensor_input_transpose line 57
  8. lemma OAI.SecretKey.hsAdjoint_tensor_effect line 63
  9. lemma OAI.SecretKey.pullback_tensor line 81
  10. lemma OAI.SecretKey.hsAdjoint_ad_comp line 89