# Zulip Chat Archive

## Stream: maths

### Topic: Polynomials over a field are not quite Euclidean in lean

#### Chris Hughes (May 28 2018 at 09:16):

I've been trying to prove polynomials over a field are a Euclidean domain. The only trouble is, they do not meet the axioms if I use degree as valuation since for two constant polynomials, degree (a % b) = degree b. Does anyone have experience doing this in any other theorem prover and can recommend a sensible solution. The most obvious is to define`new_degree 0 = 0`

, and `new_degree p = degree p + 1`

for `p ≠ 0`

. Is this the best option?

#### Johannes Hölzl (May 28 2018 at 09:23):

In Isabelle the size is not degree `d`

itself but `2^d`

, and 0 for the 0 polynomial. See http://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Polynomial_Factorial.html :

definition euclidean_size_field_poly :: "'a :: field poly ⇒ nat" where "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)"

#### Chris Hughes (May 28 2018 at 09:24):

Why `2^d`

?

#### Johan Commelin (May 28 2018 at 09:26):

I actually think that `valuation_remainder_lt`

is not what mathematicians want

#### Johan Commelin (May 28 2018 at 09:27):

It is a lot stronger than the usual condition

#### Johan Commelin (May 28 2018 at 09:27):

They swapped two quantifiers, so to speak

#### Mario Carneiro (May 28 2018 at 09:28):

what do you mean?

#### Johan Commelin (May 28 2018 at 09:28):

Quote from wiki: (EF1) If a and b are in R and b is nonzero, then there are q and r in R such that a = bq + r and either r = 0 or f(r) < f(b).

#### Johannes Hölzl (May 28 2018 at 09:28):

Why

`2^d`

?

I guess you get the nice rule: `E(p * q) = E(p) * E (q)`

#### Mario Carneiro (May 28 2018 at 09:29):

oh, you need `a % b != 0`

also as a precondition

#### Johan Commelin (May 28 2018 at 09:29):

So it is about the existence of q and r, but this somehow requires it for all q and r

#### Johannes Hölzl (May 28 2018 at 09:29):

(where `E = euclidean_size_field_poly`

)

#### Johan Commelin (May 28 2018 at 09:29):

Mario, I think that would also fix it, yes.

#### Mario Carneiro (May 28 2018 at 09:30):

that's basically what wiki is saying, or you can have a disjunction at the end

#### Johan Commelin (May 28 2018 at 09:30):

After all, the valuation of 0 is `37`

according to @Kevin Buzzard

#### Mario Carneiro (May 28 2018 at 09:30):

hey, with the new `with_zero`

class you can now just say that `valuation`

takes values in `with_zero nat`

#### Johan Commelin (May 28 2018 at 09:31):

Nooo! `with_zero nat`

looks horrible... can we please have `with_bot`

or something

#### Mario Carneiro (May 28 2018 at 09:32):

it's the absorbing element of multiplication...

#### Mario Carneiro (May 28 2018 at 09:32):

there is also with_bot, which has no algebraic interpretation

#### Mario Carneiro (May 28 2018 at 09:33):

actually `valuation`

looks like it doesn't need any algebraic interpretation, so I guess `with_bot`

is fine

#### Chris Hughes (May 28 2018 at 09:34):

It could just be generalised to take any well founded relation, instead of a valuation

#### Chris Hughes (May 28 2018 at 17:58):

hey, with the new

`with_zero`

class you can now just say that`valuation`

takes values in`with_zero nat`

Where is this class defined? I definitely prefer the idea of option nat over 2^degree.

#### Mario Carneiro (May 28 2018 at 19:30):

`with_bot`

is in `lattice.bounded_lattice`

, `with_zero`

is in `algebra.group`

. Basically it should already be available if you have the basic mathlib lemmas

Last updated: May 09 2021 at 09:11 UTC