Library mathcomp.algebra.ssrnum

Number structures NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This file defines some classes to manipulate number structures, i.e, structures with an order and a norm. To use this file, insert "Import Num.Theory." before your scripts. You can also "Import Num.Def." to enjoy shorter notations (e.g., minr instead of Num.min, lerif instead of Num.leif, etc.). This file defines the following number structures: porderZmodType == join of Order.POrder and GRing.Zmodule The HB class is called POrderedZmodule. normedZmodType == Zmodule with a norm The HB class is called NormedZmodule. numDomainType == Integral domain with an order and a norm The HB class is called NumDomain. numFieldType == Field with an order and a norm The HB class is called NumField. numClosedFieldType == Partially ordered Closed Field with conjugation The HB class is called ClosedField. realDomainType == Num domain where all elements are positive or negative The HB class is called RealDomain. realFieldType == Num Field where all elements are positive or negative The HB class is called RealField. rcfType == A Real Field with the real closed axiom The HB class is called RealClosedField. The ordering symbols and notations (<, <=, >, >=, _ <= _ ?= iff _, _ < _ ?<= if _, >=<, and ><) and lattice operations (meet and join) defined in order.v are redefined for the ring_display in the ring_scope (%R). 0-ary ordering symbols for the ring_display have the suffix "%R", e.g., <%R. All the other ordering notations are the same as order.v. Over these structures, we have the following operations: `|x| == norm of x Num.sg x == sign of x: equal to 0 iff x = 0, to 1 iff x > 0, and to -1 in all other cases (including x < 0) x \is a Num.pos <=> x is positive (:= x > 0) x \is a Num.neg <=> x is negative (:= x < 0) x \is a Num.nneg <=> x is positive or 0 (:= x >= 0) x \is a Num.npos <=> x is negative or 0 (:= x <= 0) x \is a Num.real <=> x is real (:= x >= 0 or x < 0) Num.sqrt x == in a real-closed field, a positive square root of x if x >= 0, or 0 otherwise For numeric algebraically closed fields we provide the generic definitions 'i == the imaginary number (:= sqrtC (-1)) 'Re z == the real component of z 'Im z == the imaginary component of z z^* == the complex conjugate of z (:= conjC z) sqrtC z == a nonnegative square root of z, i.e., 0 <= sqrt x if 0 <= x n.-root z == more generally, for n > 0, an nth root of z, chosen with a minimal non-negative argument for n > 1 (i.e., with a maximal real part subject to a nonnegative imaginary part) Note that n.-root (-1) is a primitive 2nth root of unity, an thus not equal to -1 for n odd > 1 (this will be shown in file cyclotomic.v).

• list of prefixes : p : positive n : negative sp : strictly positive sn : strictly negative i : interior = in [0, 1] or ]0, 1[ e : exterior = in [1, +oo[ or ]1; +oo[ w : non strict (weak) monotony

Pdeg2.NumClosed : theory of the degree 2 polynomials on NumClosedField. Pdeg2.NumClosedMonic : theory of Pdeg2.NumClosed specialized to monic polynomials. Pdeg2.Real : theory of the degree 2 polynomials on RealField and rcfType. Pdeg2.RealMonic : theory of Pdeg2.Real specialized to monic polynomials.

Notation " [ 'normedZmodType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun) (at level 0, format " [ 'normedZmodType' R 'of' T 'for' cT ]") : form_scope. Notation " [ 'normedZmodType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id) (at level 0, format " [ 'normedZmodType' R 'of' T ]") : form_scope.

TODO: make isNumDomain depend on intermediate structures TODO: make isNumDomain.sort canonically a NumDomain

Shorter qualified names, when Num.Def is not imported.

(Exported) symbolic syntax.

The rest of the numbers interface hierarchy.