OAI/NumberTheory/Ostmann/Construction/FixedPivotPairSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Both histories retain their large-prime support under the original law

  1. theorem OAI.Ostmann.word_prime_pair_checks_fixed_pivot_bound line 12