OAI/Analysis/MutuallyUnbiased/TaoCertificate/KnownTarget0.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.knownParams0line 8 - def
OAI.MUB6.TaoCertificate.knownTarget0line 10 - theorem
OAI.MUB6.TaoCertificate.knownTarget0_checkedline 12 - theorem
OAI.MUB6.TaoCertificate.knownParams0_validline 15 - theorem
OAI.MUB6.TaoCertificate.knownTarget0_valueline 20