Stream: general

Topic: Proving field is gcd domain

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)⁻¹...

AHan (Dec 19 2018 at 09:40):

Do I misunderstand something?

Kenny Lau (Dec 19 2018 at 09:41):

therefore gcd a b = 1!

AHan (Dec 19 2018 at 09:42):

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

why?

Kenny Lau (Dec 19 2018 at 09:42):

who would say that gcd 3 5 = -1?

Kenny Lau (Dec 19 2018 at 09:42):

or gcd pi e = 3?

AHan (Dec 19 2018 at 09:48):

Why wouldn't gcd 3 5 = 3 ?

Oh I'm wrong...

AHan (Dec 19 2018 at 09:49):

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

Last updated: May 17 2021 at 22:15 UTC