OAI/Analysis/MutuallyUnbiased/TaoCertificate/CubeTarget.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.cubeTargetline 8 - theorem
OAI.MUB6.TaoCertificate.cubeTarget_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.cubeTarget_valueline 12