Zulip Chat Archive

Stream: general

Topic: Proving field is gcd domain


view this post on Zulip AHan (Dec 19 2018 at 09:39):

While trying to prove a field is gcd domain, I found out that there seems like a conflict between two fields of class gcd_domain to me ...
lean norm_unit_coe_units : ∀(u : units α), norm_unit u = u⁻¹ and
lean norm_unit_gcd : ∀a b, norm_unit (gcd a b) = 1
Since every element in a field, is a unit, and if a ≠ 0 ∨ b ≠ 0, then 1 = norm_unit (gcd a b) = (gcd a b)⁻¹...

view this post on Zulip AHan (Dec 19 2018 at 09:40):

Do I misunderstand something?

view this post on Zulip Kenny Lau (Dec 19 2018 at 09:41):

therefore gcd a b = 1!

view this post on Zulip AHan (Dec 19 2018 at 09:42):

@Kenny Lau Yes... which sounds strange to me...

view this post on Zulip Kenny Lau (Dec 19 2018 at 09:42):

why?

view this post on Zulip Kenny Lau (Dec 19 2018 at 09:42):

who would say that gcd 3 5 = -1?

view this post on Zulip Kenny Lau (Dec 19 2018 at 09:42):

or gcd pi e = 3?

view this post on Zulip AHan (Dec 19 2018 at 09:48):

Why wouldn't gcd 3 5 = 3 ?

view this post on Zulip AHan (Dec 19 2018 at 09:49):

Oh I'm wrong...

view this post on Zulip AHan (Dec 19 2018 at 09:49):

Yeah, you're right! It sould be 1!!


Last updated: May 17 2021 at 22:15 UTC