OAI/Analysis/MutuallyUnbiased/TaoCertificate/KnownTarget4.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.knownParams4line 8 - def
OAI.MUB6.TaoCertificate.knownTarget4line 10 - theorem
OAI.MUB6.TaoCertificate.knownTarget4_checkedline 12 - theorem
OAI.MUB6.TaoCertificate.knownParams4_validline 15 - theorem
OAI.MUB6.TaoCertificate.knownTarget4_valueline 20