OAI/InformationTheory/Entanglement/SecretDefinitions.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SecretKey.traceNormline 17 - def
OAI.SecretKey.Representedline 21
OAI/InformationTheory/Entanglement/SecretDefinitions.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.SecretKey.traceNorm line 17OAI.SecretKey.Represented line 21