OAI/Computability/QuantumFactoring/TableFavorable.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.table_pairwise_iff line 17
2. def OAI.ExactQuantumFactoring.tableFavorable line 33

   Source documentation

   Pairwise comparison avoids searching for a least component. The supplied rectangular table may contain duplicates and harmless primes not dividing m.

   noncomputable def tableFavorable (ps : List ℕ) (data : FactorData) (a m n : ℕ) : Prop :=
   …

   Mentions: OAI.ExactQuantumFactoring.FactorData

3. lemma OAI.ExactQuantumFactoring.tableFavorable_correct line 38