OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionFinalArithmetic.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.Certificate.MixedTargetSemantics.numericRawPolynomialline 11 - theorem
OAI.MUB6.Certificate.MixedTargetSemantics.numericRawPolynomialEvalline 13 - theorem
OAI.MUB6.Certificate.MixedTargetSemantics.originalReductionCheckline 19 - theorem
OAI.MUB6.Certificate.MixedTargetSemantics.numericReductionCheckline 21 - theorem
OAI.MUB6.Certificate.MixedTargetSemantics.numericReductionEvalline 24