euclidean domain

Stream: maths

[Johan Commelin]

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]

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]

Good catch!

[Johan Commelin]

Chris and Lean helped me prove a theorem!

[Chris Hughes]

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

[Reid Barton]

Both a theorem, and a counterexample :slight_smile:

[Johan Commelin]

Haha, sure. Zerology bites me again.

[Chris Hughes]

Maybe it should extend nonzero_comm_ring instead.

[Johan Commelin]

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]

Maybe we should just have euclidean.core and then of_core... that seems to be a common trick.

[Chris Hughes]

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

[Johan Commelin]

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

[Chris Hughes]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Hughes]

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]

Ok, good.

[Chris Hughes]

This worked when I tried changing integral domain.

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

[Johan Commelin]

Great!