Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 18:26):

mod_X_sub_C_eq_C_eval

view this post on Zulip 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"

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:27):

Could we extract a witness using unique choice?

view this post on Zulip Reid Barton (Jun 02 2020 at 18:28):

Yes but only noncomputably

view this post on Zulip Johan Commelin (Jun 02 2020 at 18:28):

instance : fintype mathlib

view this post on Zulip 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"

view this post on Zulip Patrick Massot (Jun 02 2020 at 18:46):

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

view this post on Zulip Patrick Massot (Jun 02 2020 at 18:48):

They mean https://en.wikipedia.org/wiki/B%C3%A9zout%27s_identity

view this post on Zulip Reid Barton (Jun 02 2020 at 18:57):

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

view this post on Zulip Reid Barton (Jun 02 2020 at 19:03):

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

view this post on Zulip Patrick Massot (Jun 02 2020 at 19:07):

We certainly have the version for integer, even computationaly.

view this post on Zulip Patrick Massot (Jun 02 2020 at 19:07):

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

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 19:22):

Aargh

view this post on Zulip Kevin Buzzard (Jun 02 2020 at 19:22):

But there is one for Euclidean domains I think

view this post on Zulip 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