Bézout's identity for a finite family of natural numbers

If natural numbers f i, i ∈ s, have greatest common divisor 1 in ℕ, then some integer combination of them is 1. Mathlib's Finset.gcd_eq_sum_mul gives this for the gcd computed in ℤ; this file transfers the hypothesis from ℕ, where it is usually established, for instance by Finset.gcd_div_eq_one.

Main results

• Finset.exists_sum_natCast_mul_eq_one_of_gcd_eq_one: if s.gcd f = 1 in ℕ, then ∑ i ∈ s, f i * c i = 1 for some c : ι → ℤ.

theorem Finset.exists_sum_natCast_mul_eq_one_of_gcd_eq_one {ι : Type u_1} {s : Finset ι} {f : ι → ℕ} (h : s.gcd f = 1) : ∃ (c : ι → ℤ), ∑ i ∈ s, ↑(f i) * c i = 1

Bézout's identity for natural numbers: if f i, i ∈ s, have greatest common divisor 1, then some integer combination ∑ i ∈ s, f i * c i is 1.