OAI/InformationTheory/Entanglement/PhysicalRightStep.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SecretKey.IsRightTraceAction line 15
2. lemma OAI.SecretKey.physical_right_born line 20
3. lemma OAI.SecretKey.physical_right_disintegration line 29
4. lemma OAI.SecretKey.physical_right_disintegration_all line 46
5. lemma OAI.SecretKey.physical_right_outcome line 81
6. def OAI.SecretKey.physical_right_update line 94