Thue's lemma

TheoremThue's lemma, general form#✓fully proved

Let \(a\) and \(n\) be integers with \(n > 1\) and \(\gcd(a, n) = 1\). Then there exist nonzero integers \(x\) and \(y\) with \(|x| < \sqrt{n}\), \(|y| < \sqrt{n}\) and \(x \equiv a y \pmod{n}\). Unlike the source form of Thue's lemma, no lower bound on \(a\) is assumed.

theorem thue_lemma_general (a n : ℤ) (hn : 1 < n) (hcop : Int.gcd a n = 1) :
    ∃ x y : ℤ,
      (0 : ℤ) < |x| ∧ (|x| : ℝ) < Real.sqrt (n : ℝ) ∧
      (0 : ℤ) < |y| ∧ (|y| : ℝ) < Real.sqrt (n : ℝ) ∧ x ≡ a * y [ZMOD n]

Used by 1

Used byThue's lemma

TheoremThue's lemma#✓fully proved

Let \(a\) and \(n\) be integers with \(a > 1\), \(n > 1\) and \(\gcd(a, n) = 1\). Then there exist nonzero integers \(x\) and \(y\) with \(|x| < \sqrt{n}\), \(|y| < \sqrt{n}\) and \(x \equiv a y \pmod{n}\).

The hypothesis \(a > 1\) follows the source and is not needed for the conclusion.

theorem thue_lemma (a n : ℤ) (ha : 1 < a) (hn : 1 < n)
    (hcop : Int.gcd a n = 1) :
    ∃ x y : ℤ,
      (0 : ℤ) < |x| ∧ (|x| : ℝ) < Real.sqrt (n : ℝ) ∧
      (0 : ℤ) < |y| ∧ (|y| : ℝ) < Real.sqrt (n : ℝ) ∧ x ≡ a * y [ZMOD n]

Sources

• Bencheng Li, Steven J. Miller, Tudor Popescu, Daniel Sarnecki, and Nawapan Wattanawanichkul, "Modeling Random Walks to Infinity on Primes in Z[√2]", Journal of Integer Sequences 25 (2022), Article 22.6.1, Lemma [Thue's lemma], lines 217–218, https://cs.uwaterloo.ca/journals/JIS/VOL25/Miller/miller11.tex. Original: V. Shoup, "A Computational Introduction to Number Theory and Algebra", Cambridge University Press, 2005, p. 43.

Uses 1

Proof usesThue's lemma, general form

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.