Documentation

Mathlib.Algebra.EuclideanDomain.Instances

Instances for Euclidean domains #

Equations
  • One or more equations did not get rendered due to their size.
@[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)