Structures · Algebra

EuclideanDomain

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

Shape

One type argument · adds quotient, quotient_zero, remainder, quotient_mul_add_remainder_eq, r, r_wellFounded, remainder_lt, mul_left_not_lt