Bézout's identity

Stream: Is there code for X?

[Adrián Doña Mateo]

I need a generalised Bézout's identity for more than 2 integers for an IMO problem. Is there something like that in mathlib?

[Johan Commelin]

Not that I know of

[Kevin Buzzard]

What's the statement?

[Adrián Doña Mateo]

Given any integers a₁,...,aₙ there always exist integers x₁,...,xₙ such that x₁ * a₁ + ⋯ + xₙ * aₙ = gcd(a₁,...,aₙ). I believe something similar is true for principal ideal domains.

[Adrián Doña Mateo]

I don't think there is a definition of gcd for more than two elements in mathlib so seems like there can't be for this. Any thoughts on how difficult it would be to define this and prove the generalised identity?

[Aaron Anderson]

You can state this with multiset.gcd or finset.gcd

[Aaron Anderson]

And multiset has a good inductive principle, so you could prove your desired version by induction

[Aaron Anderson]

What data structure did you want to use to encode the tuple of numbers?

[Adrián Doña Mateo]

I thought finset would make the most sense

[Eric Wieser]

Seems like this would be nice to prove for multiset, from which the proof for finset ought to be obvious?

[Alex J. Best]

Here's a messy sketch of this :smile:

import algebra.big_operators
open int
open euclidean_domain

lemma map_mul_sum (r : ℤ) (l : list ℤ) : (l.map ((*) (r : ℤ))).sum = r * l.sum :=
by convert list.sum_hom l ⟨((*) r), mul_zero r, λ x y, mul_add r x y⟩
lemma zip_with_mul_map_mul (r : ℤ) (l₁ l₂ : list ℤ) : l₁.zip_with (*) (l₂.map ((*) (r : ℤ))) =
                                                     (l₁.zip_with (*) l₂).map ((*) (r : ℤ)) := sorry

def asd : Π (l : list ℤ), {a : list ℤ // l.foldr gcd 0 = (l.zip_with (*) a).sum }
| [] := ⟨ [], by simp ⟩
| (h :: ll) := ⟨ gcd_a h (ll.foldr gcd 0) :: ((asd ll : list ℤ).map ((*) (gcd_b h (ll.foldr gcd 0)))), begin
 simp,
 convert gcd_eq_gcd_ab _ _,
 have := (asd ll).2,
 simp [zip_with_mul_map_mul _ _ _, map_mul_sum],
 rw mul_comm,
 congr,
 exact this.symm,
end⟩
#eval asd [6, 15, 10]

[Adrián Doña Mateo]

Is it preferable to have a function to this subtype or a theorem that states the existence of such list?

[Eric Wieser]

Given that @Alex J. Best has gone to the effort of a computable construction, it seems a shame to not use it and and provide a non-computable construction via exists.

[Adrián Doña Mateo]

That makes sense, thanks!

[Eric Wieser]

Although it might make sense to split asd into

def bezout_factors (l : list ℤ) : list ℤ

lemma bezout_prop (l) :  (bezout_factors l).foldr gcd 0 = (l.zip_with (*) (bezout_factors l)).sum

but only if that makes the definition simpler