Instances for Euclidean domains

• Field.toEuclideanDomain: shows that any field is a Euclidean domain.

@[instance 100]

instance Field.toEuclideanDomain {K : Type u_1} [Field K] : EuclideanDomain K

Equations

• Field.toEuclideanDomain = EuclideanDomain.mk (fun (x1 x2 : K) => x1 / x2) ⋯ (fun (a b : K) => a - a * b / b) ⋯ (fun (a b : K) => a = 0 ∧ b ≠ 0) ⋯ ⋯ ⋯