Proving field is gcd domain

Stream: general

[AHan]

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]

Do I misunderstand something?

[Kenny Lau]

therefore gcd a b = 1!

[AHan]

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

[Kenny Lau]

why?

[Kenny Lau]

who would say that gcd 3 5 = -1?

[Kenny Lau]

or gcd pi e = 3?

[AHan]

Why wouldn't gcd 3 5 = 3 ?

[AHan]

Oh I'm wrong...

[AHan]

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