## Stream: Is there code for X?

### Topic: Bézout's identity

#### Adrián Doña Mateo (Jan 11 2021 at 16:54):

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 (Jan 11 2021 at 17:10):

Not that I know of

#### Kevin Buzzard (Jan 11 2021 at 17:17):

What's the statement?

#### Adrián Doña Mateo (Jan 11 2021 at 17:22):

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 (Jan 11 2021 at 17:26):

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 (Jan 11 2021 at 17:28):

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

#### Aaron Anderson (Jan 11 2021 at 17:29):

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

#### Aaron Anderson (Jan 11 2021 at 17:30):

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

#### Adrián Doña Mateo (Jan 11 2021 at 17:31):

I thought finset would make the most sense

#### Eric Wieser (Jan 11 2021 at 17:32):

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

#### Alex J. Best (Jan 11 2021 at 19:12):

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 (Jan 12 2021 at 11:43):

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

#### Eric Wieser (Jan 12 2021 at 11:44):

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 (Jan 12 2021 at 11:45):

That makes sense, thanks!

#### Eric Wieser (Jan 12 2021 at 11:47):

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

Last updated: May 16 2021 at 05:21 UTC