## Stream: Is there code for X?

### Topic: f(x)=q(x)(x-r) + f(r)

#### Kevin Buzzard (Jun 02 2020 at 18:25):

Do we know that the remainder when we divide f(x) by (x-r) is f(r)? I am guessing that this is "Bezout's theorem" here

#### Kevin Buzzard (Jun 02 2020 at 18:26):

mod_X_sub_C_eq_C_eval

#### Reid Barton (Jun 02 2020 at 18:27):

I was going to give a nonconstructive "yes, I saw Chris use it in the solution to some kata"

#### Johan Commelin (Jun 02 2020 at 18:27):

Could we extract a witness using unique choice?

#### Reid Barton (Jun 02 2020 at 18:28):

Yes but only noncomputably

#### Johan Commelin (Jun 02 2020 at 18:28):

instance : fintype mathlib

#### Reid Barton (Jun 02 2020 at 18:28):

Just put on the web page "the lemma Reid saw once in some kata solution by Chris"

#### Patrick Massot (Jun 02 2020 at 18:46):

No, this is not what Bézout refers to here

#### Reid Barton (Jun 02 2020 at 18:57):

I think this came up recently and the answer was we didn't have exactly this

#### Reid Barton (Jun 02 2020 at 19:03):

(but we really should, particularly the "more generally" part)

#### Patrick Massot (Jun 02 2020 at 19:07):

We certainly have the version for integer, even computationaly.

#### Patrick Massot (Jun 02 2020 at 19:07):

But the expected version in this context is the one for PID.

Aargh

#### Kevin Buzzard (Jun 02 2020 at 19:22):

But there is one for Euclidean domains I think

#### Chris Hughes (Jun 02 2020 at 19:45):

The content of proving that for integers is not really proving it for a PID, but proving the integers are a PID.

Last updated: May 16 2021 at 05:21 UTC