Theorems · Inductive type · commutative algebra

EuclideanDomain

Type u → Type u

A EuclideanDomain is a non-trivial commutative ring with a division and a remainder, satisfying b * (a / b) + a % b = a. The definition of a Euclidean domain usually includes a valuation function R → ℕ. This definition is slightly generalised to include a well-founded relation r with the property that r (a % b) b, instead of a valuation.

Defined in

Mathlib.Algebra.EuclideanDomain.Defs

Cited by

124 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms