Subsections

• Arithmetic Operations
• Equality and Membership
• Parent and Category
• Predicates on Ring Elements
• Other Element Functions

+ v : RngValElt -> RngValElt

- v : RngValElt -> RngValElt

v + w : RngValElt, RngValElt -> RngValElt

v - w : RngValElt, RngValElt -> RngValElt

v * w : RngValElt, RngValElt -> RngValElt

v ^ k : RngValElt, RngIntElt -> RngValElt

v / w : RngValElt, RngValElt -> RngValElt

v +:= w : RngValElt, RngValElt -> RngValElt

v -:= w : RngValElt, RngValElt -> RngValElt

v *:= w : RngValElt, RngValElt -> RngValElt

The quotient q of the division with remainder v=qw + r, where the remainder will have valuation less than that of w; if the valuation of v is greater than or equal than that of w, this simply returns the quotient v/w, if the valuation of w exceeds that of v it returns 0.

v eq w : RngValElt, RngValElt -> BoolElt

v ne w : RngValngIntt, RngValElt -> BoolElt

v in V : RngValElt, Rng -> BoolElt

v notin V : RngValElt, Rng -> BoolElt

Parent(v) : RngValElt -> RngVal

Category(v) : RngValElt -> Cat

IsZero(n) : RngValElt -> BoolElt

IsOne(n) : RngValElt -> BoolElt

IsMinusOne(n) : RngValElt -> BoolElt

IsNilpotent(n) : RngValElt -> BoolElt

IsIdempotent(n) : RngValElt -> BoolElt

IsUnit(n) : RngValElt -> BoolElt

IsZeroDivisor(n) : RngValElt -> BoolElt

IsRegular(n) : RngVal -> BoolElt

Valuation(v) : RngValElt -> RngIntElt

Given an element v of a valuation ring V, return the valuation (associated with V) of v.

Given two elements v, w of a valuation ring V with associated valuation phi, return a quotient and remainder q and r in V such that v=qw + r and 0 <= phi(r)<phi(w). If phi(v)<phi(w) this simply returns q=0 and r=v, and if phi(v) >= phi(w) then it returns q=v/w and r=0.

Gcd(v, w) : RngValElt, RngValElt -> RngValElt

GCD(v, w) : RngValElt, RngValElt -> RngValElt

This function returns a greatest common divisor of two elements v, w in a valuation ring V. This will return u^m, where m=min(phi(v), phi(w)) is the minimum of the valuations of v and w m=min(phi(v), phi(w)) and u is the uniformizing element of V (with valuation phi(u)=1).

Xgcd(v, w) : RngValElt, RngValElt -> RngValElt, RngValElt, RngValElt

XGCD(v, w) : RngValElt, RngValElt -> RngValElt, RngValElt, RngValElt

This function returns a greatest common divisor z in V of two elements v, w in a valuation ring V as well as multipliers x, y in V such that xv + yw=z. The principal return value will be z=u^m, where m=min(phi(v), phi(w)) is the minimum of the valuations of v and w m=min(phi(v), phi(w)) and u is the uniformizing element of V (with valuation phi(u)=1).