Zulip Chat Archive

Stream: maths

Topic: euclidean domain


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

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:57):

Good catch!

view this post on Zulip Johan Commelin (Nov 15 2018 at 13:58):

Chris and Lean helped me prove a theorem!

view this post on Zulip Chris Hughes (Nov 15 2018 at 14:18):

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

view this post on Zulip Reid Barton (Nov 15 2018 at 14:21):

Both a theorem, and a counterexample :slight_smile:

view this post on Zulip Johan Commelin (Nov 15 2018 at 14:33):

Haha, sure. Zerology bites me again.

view this post on Zulip Chris Hughes (Nov 15 2018 at 16:42):

Maybe it should extend nonzero_comm_ring instead.

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

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

view this post on Zulip Chris Hughes (Nov 15 2018 at 17:30):

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 17:31):

Why would they be defeq? Because integral_domain extends comm_ring by a Prop?

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 17:35):

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

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

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 17:36):

Ok, good.

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

view this post on Zulip Johan Commelin (Nov 15 2018 at 18:41):

Great!


Last updated: May 18 2021 at 07:19 UTC