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

Stream: Is there code for X?

[Kevin Buzzard]

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]

mod_X_sub_C_eq_C_eval

[Reid Barton]

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

[Johan Commelin]

Could we extract a witness using unique choice?

[Reid Barton]

Yes but only noncomputably

[Johan Commelin]

instance : fintype mathlib

[Reid Barton]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Reid Barton]

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

[Reid Barton]

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

[Patrick Massot]

We certainly have the version for integer, even computationaly.

[Patrick Massot]

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

[Kevin Buzzard]

Aargh

[Kevin Buzzard]

But there is one for Euclidean domains I think

[Chris Hughes]

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