# Zulip Chat Archive

## Stream: maths

### Topic: euclidean domains

#### Johan Commelin (Jul 20 2018 at 07:25):

Currently, the definition of a Euclidean domain has the field

(val_remainder_lt : ∀ a {b}, b ≠ 0 → valuation (remainder a b) < valuation b)

I think it should read

(val_remainder_lt : ∀ a {b}, b ≠ 0 → (remainder a b = 0 ∨ valuation (remainder a b) < valuation b))

or something like that. What is best in these cases:

(i) the change as I suggest, or

(ii) move the claim `remainder a b = 0`

to a condition, so `b \ne 0 \and remainder a b \ne 0 \to ...`

#### Chris Hughes (Jul 20 2018 at 07:35):

My plan when I wrote polynomials, was that it should take a well founded relation instead of a valuation. `mod_lt`

would be `r (remainder a b) b`

and `val_me_mul_left`

would be `not r (a * b) a`

I think. `degree`

now returns `with_bot nat`

so it meets this definition.

#### Chris Hughes (Jul 20 2018 at 07:44):

The trouble with your definition is it makes every proof and definition longer. For example gcd needs an extra `else if`

.

def gcd : α → α → α | a := λ b, if a0 : a = 0 then b else if hba : remainder b a = 0 then a else have h:_ := or.resolve_left (val_mod_lt' b a0) hba, gcd (b%a) a using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf valuation⟩]}

#### Johan Commelin (Jul 20 2018 at 08:02):

On the other hand, it is the definition that every mathematician is used to...

#### Johan Commelin (Jul 20 2018 at 08:02):

@Chris Hughes Do you think the `valuation`

of an ED should also take values in `with_bot nat`

? And then require that `valuation a = bot \iff a = 0`

?

#### Chris Hughes (Jul 20 2018 at 08:04):

That might be also be an idea, but without `valuation a = bot \iff a = 0`

, because that will be annoying with integers.

#### Chris Hughes (Jul 20 2018 at 08:05):

But even so, I think arbitrary well founded is better, because then people dealing with integers can use the relation `x.nat_abs < y.nat_abs`

where the use of `with_bot`

would just be annoying.

#### Johan Commelin (Jul 20 2018 at 09:54):

So, what do you suggest as definition of ED?

#### Johan Commelin (Jul 20 2018 at 09:54):

Then we can try to use that, and also prove that it is equivalent to the "usual" definition. And possibly build a 2nd constructor that mimics the "usual" one.

#### Chris Hughes (Jul 20 2018 at 11:54):

I just made a PR with my suggested solution. https://github.com/leanprover/mathlib/pull/211

#### Johan Commelin (Jul 20 2018 at 12:04):

Nice! I like your speed!

#### Johan Commelin (Jul 20 2018 at 13:14):

Cool, you add an instance for `int`

!

Last updated: May 10 2021 at 08:14 UTC