OAI/InformationTheory/Entanglement/Coherence.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SecretKey.four_effect_commutingline 14 - theorem
OAI.SecretKey.four_effectline 83
OAI/InformationTheory/Entanglement/Coherence.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.SecretKey.four_effect_commuting line 14OAI.SecretKey.four_effect line 83