OAI/NumberTheory/Ostmann/Quadratic/QuadraticGcdCorrectionPowerSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A small-power bound for the complete original gcd correction

  1. theorem OAI.Ostmann.quadratic_gcd_corrections_power_bound line 11