OAI/NumberTheory/Ostmann/Arithmetic/JointSampledComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint signed replacement with actual internal-prime coordinates

Different tests can use different sampled primes and can depend on the other prime coordinates. Each test only excludes its own prime coordinate.

  1. theorem OAI.Ostmann.joint_sampled_polynomial_comparison_le line 15