Theorems · Theorem · number theory

Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le

∀ (p q n : ℕ), p.gcd q ∣ n → p.pred * q.pred ≤ n → ∃ a b, a * p + b * q = n

If the gcd of two natural numbers p and q divides a third natural number n, and if n is at least (p - 1) * (q - 1), then n can be represented as an ℕ-linear combination of p and q. TODO: show that if p.gcd q = 1 and 0 ≤ n ≤ (p - 1) * (q - 1) - 1 = N, then n is representable iff N - n is not. In particular N is not representable, solving the coin problem for two coins: https://en.wikipedia.org/wiki/Coin_problem#n_=_2.

Defined in

Mathlib.Algebra.Order.Ring.Int

Cited by

3 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound