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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Field.mod_eq {K : Type u_1} [Field K] (a b : K) : a % b = a - a * b / b

@[simp]

theorem Field.gcd_eq {K : Type u_1} [Field K] [DecidableEq K] (a b : K) : EuclideanDomain.gcd a b = if a = 0 then b else a

theorem Field.gcd_zero_eq {K : Type u_1} [Field K] [DecidableEq K] (b : K) : EuclideanDomain.gcd 0 b = b

theorem Field.gcd_eq_of_ne {K : Type u_1} [Field K] [DecidableEq K] {a : K} (ha : a ≠ 0) (b : K) : EuclideanDomain.gcd a b = a