OAI/NumberTheory/JointDickman/Arithmetic/TruncatedPrimeHyperbola.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rational cancellation after removing both small bilinear variables

  1. def OAI.JointDickman.truncatedPrimeHyperbola line 10
  2. theorem OAI.JointDickman.truncated_prime_hyperbola_bound line 14