Documentation

Mathlib.Algebra.EuclideanDomain.Field

Instances for Euclidean domains #

@[instance 100]
Equations
  • Field.toEuclideanDomain = EuclideanDomain.mk (fun (x x_1 : K) => x / x_1) (fun (a b : K) => a - a * b / b) (fun (a b : K) => a = 0 b 0)