# Zulip Chat Archive

## Stream: maths

### Topic: euclidean domain

#### Johan Commelin (Nov 15 2018 at 13:53):

Euclidean domains are extending integral domains, but the entire file doesn't use this. We could just as well extend `comm_ring`

. @Kevin Buzzard Do you know if every *Euclidean ring* is automatically an integral domain?

#### Chris Hughes (Nov 15 2018 at 13:57):

I think the following theorems imply they are

lemma mul_div_cancel (a) {b : α} (b0 : b ≠ 0) : (a * b) / b = a := by rw mul_comm; exact mul_div_cancel_left a b0 @[simp] lemma zero_div {a : α} (a0 : a ≠ 0) : 0 / a = 0 := by simpa only [zero_mul] using mul_div_cancel 0 a0

#### Johan Commelin (Nov 15 2018 at 13:57):

Good catch!

#### Johan Commelin (Nov 15 2018 at 13:58):

Chris and Lean helped me prove a theorem!

#### Chris Hughes (Nov 15 2018 at 14:18):

Wait, I was wrong. There's no way to prove `zero_ne_one`

.

#### Reid Barton (Nov 15 2018 at 14:21):

Both a theorem, and a counterexample :slight_smile:

#### Johan Commelin (Nov 15 2018 at 14:33):

Haha, sure. Zerology bites me again.

#### Chris Hughes (Nov 15 2018 at 16:42):

Maybe it should extend `nonzero_comm_ring`

instead.

#### Johan Commelin (Nov 15 2018 at 17:25):

Wouldn't that create a possibility for diamonds? Say we prove that integral closures are integral domains. And then for certain of those we prove that they are euclidean rings. And then this would give a new proof that those things are integral domains...

#### Johan Commelin (Nov 15 2018 at 17:26):

Maybe we should just have `euclidean.core`

and then `of_core`

... that seems to be a common trick.

#### Chris Hughes (Nov 15 2018 at 17:30):

Yes, but they would be definitionally equal diamonds, which happen all the time and are fine.

#### Johan Commelin (Nov 15 2018 at 17:31):

Why would they be defeq? Because `integral_domain`

extends `comm_ring`

by a `Prop`

?

#### Chris Hughes (Nov 15 2018 at 17:34):

But all the fields would be the same, because they all come from the same place ultimately.

#### Johan Commelin (Nov 15 2018 at 17:35):

No we would have two different proofs that certain rings are integral domains...

#### Johan Commelin (Nov 15 2018 at 17:35):

One coming from the fact that it's an integral closure, the other from the fact that it is a euclidean ring

#### Chris Hughes (Nov 15 2018 at 17:35):

Proofs are irrelevant.

The same thing happens with say, polynomials over an integral domain are an integral domain which means they're a ring, but polynomials over a ring are a ring. So there's two different paths, but they're defeq.

#### Johan Commelin (Nov 15 2018 at 17:36):

Ok, good.

#### Chris Hughes (Nov 15 2018 at 17:43):

This worked when I tried changing integral domain.

example : euclidean_domain.integral_domain ℤ = linear_ordered_comm_ring.to_integral_domain := rfl

#### Johan Commelin (Nov 15 2018 at 18:41):

Great!

Last updated: May 18 2021 at 07:19 UTC