Module mathcomp.algebra.numeric_hierarchy.ssrnum
From mathcomp Require Export orderedzmod numdomain numfield.
Number structures
The files in this directory define classes to manipulate number
structures, i.e., structures with an order and a norm. To use these files,
insert:
"From mathcomp Require Import ssrnum."
at the top your development and
"Import Num.Theory."
before your scripts.
In addition, you can insert
"Import Num.Def."
before your scripts to enjoy shorter notations, e.g.:
- minr instead of Num.min,
- lerif instead of Num.leif,
- conjC instead of Num.conj, etc.
Module Num.
Export orderedzmod.Num.
Export numdomain.Num.
Export numfield.Num.
Module Theory.
Export Num.Theory.
End Theory.
Module Def.
Export Num.Def.
End Def.
Module ExtraDef.
#[deprecated(since="mathcomp 2.5.0", use=Num.Def.sqrtr)]
Notation sqrtr := numfield.Num.Def.sqrtr.
End ExtraDef.
End Num.