OAI/Computability/QuantumFactoring/TrialRetentionBounds.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ExactQuantumFactoring.OrderTrial.firstRetentionline 13 - lemma
OAI.ExactQuantumFactoring.OrderTrial.first_remainder_boundsline 16 - lemma
OAI.ExactQuantumFactoring.OrderTrial.all_retention_boundsline 29