N (Abbreviations)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
N (Abbreviations)
n [abbrev, in mathcomp.group_representation.mxrepresentation]n [abbrev, in mathcomp.group_representation.mxrepresentation]
n [abbrev, in mathcomp.group_representation.mxabelem]
n [abbrev, in mathcomp.group_representation.mxabelem]
n [abbrev, in mathcomp.field.fieldext]
n [abbrev, in mathcomp.field.fieldext]
n [abbrev, in mathcomp.boot.fintype]
n [abbrev, in mathcomp.algebra.vector]
n [abbrev, in mathcomp.algebra.mxpoly]
n [abbrev, in mathcomp.algebra.mxpoly]
n [abbrev, in mathcomp.algebra.matrix]
n [abbrev, in mathcomp.algebra.matrix]
n' [abbrev, in mathcomp.group_representation.mxabelem]
n_comp [abbrev, in mathcomp.boot.fingraph]
nat_def [abbrev, in mathcomp.algebra.interval_inference]
nat_spec [abbrev, in mathcomp.algebra.interval_inference]
NatTrec.doublen [abbrev, in mathcomp.boot.ssrnat]
NatTrec.oddn [abbrev, in mathcomp.boot.ssrnat]
natTrecE [abbrev, in mathcomp.boot.ssrnat]
nG [abbrev, in mathcomp.group_representation.mxrepresentation]
nG [abbrev, in mathcomp.group_representation.mxrepresentation]
Nil [abbrev, in mathcomp.boot.seq]
Nirr [abbrev, in mathcomp.group_representation.character]
nosimpl [abbrev, in mathcomp.boot.ssreflect]
nR [abbrev, in mathcomp.algebra.interval_inference]
nR [abbrev, in mathcomp.algebra.interval_inference]
nR [abbrev, in mathcomp.algebra.interval_inference]
nR [abbrev, in mathcomp.algebra.interval_inference]
nth [abbrev, in mathcomp.boot.seq]
num [abbrev, in mathcomp.algebra.interval_inference]
num [abbrev, in mathcomp.algebra.interval_inference]
num [abbrev, in mathcomp.algebra.interval_inference]
Num.Add_isHomo [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Add_isHomo.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Add_isHomo.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.ArchiClosedField [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiClosedField.clone [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiClosedField.copy [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiClosedField.Exports.archiClosedFieldType [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiClosedField.on [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiClosedField.on_ [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiDomain [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiDomain.copy [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiDomain.on [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiDomain.type [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiField [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiField.copy [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiField.on [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiField.type [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumDomain [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumDomain.clone [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumDomain.copy [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumDomain.Exports.archiNumDomainType [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumDomain.on [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumDomain.on_ [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumField [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumField.clone [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumField.copy [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumField.Exports.archiNumFieldType [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumField.on [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiNumField.on_ [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealClosedField [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealClosedField.clone [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealClosedField.copy [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealClosedField.Exports.archiRcfType [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealClosedField.on [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealClosedField.on_ [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealDomain [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealDomain.clone [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealDomain.copy [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealDomain.Exports.archiRealDomainType [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealDomain.on [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealDomain.on_ [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealField [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealField.clone [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealField.copy [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealField.Exports.archiRealFieldType [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealField.on [abbrev, in mathcomp.algebra.archimedean]
Num.ArchiRealField.on_ [abbrev, in mathcomp.algebra.archimedean]
Num.Builders_1.ler_normD [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_1.nonneg [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Builders_1.nonneg0 [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Builders_1.nonneg_definite [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Builders_1.nonnegD [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Builders_1.norm [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_1.normr0_eq0 [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_1.normrMn [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_1.normrN [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_19.int_num [abbrev, in mathcomp.algebra.archimedean]
Num.Builders_19.intrE [abbrev, in mathcomp.algebra.archimedean]
Num.Builders_19.nat_num [abbrev, in mathcomp.algebra.archimedean]
Num.Builders_19.natrE [abbrev, in mathcomp.algebra.archimedean]
Num.Builders_19.truncn [abbrev, in mathcomp.algebra.archimedean]
Num.Builders_46.addr_gt0 [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_46.ger_total [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_46.le_def [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_46.lt_def [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_46.norm [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_46.norm_eq0 [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_46.normD [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_46.normM [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_46.Rle [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_46.Rlt [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_59.real [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.ge0_norm [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.le [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.le0_add [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.le0_anti [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.le0_mul [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.le0_total [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.lt [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.lt_def [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.norm [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.normN [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.Rle [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.Rlt [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_67.sub_ge0 [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_8.addr_gt0 [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_8.ger_leVge [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_8.ler_def [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_8.normrM [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.ge0_norm [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.le [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.le_def [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.lt [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.lt0_add [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.lt0_mul [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.lt0_ngt0 [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.lt0_total [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.norm [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.normN [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.Rle [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.Rlt [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Builders_83.sub_gt0 [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.ceilD [abbrev, in mathcomp.algebra.archimedean]
Num.ClosedField [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.ClosedField.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.ClosedField.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.ClosedField.Exports.numClosedFieldType [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.ClosedField.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.ClosedField.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.comparable [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.conj_op [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.Def.archi_bound [abbrev, in mathcomp.algebra.archimedean]
Num.Def.ceil [abbrev, in mathcomp.algebra.archimedean]
Num.Def.comparabler [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.conjC [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.Def.floor [abbrev, in mathcomp.algebra.archimedean]
Num.Def.ger [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.gtr [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.int_num [abbrev, in mathcomp.algebra.archimedean]
Num.Def.ler [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.lerif [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.lterif [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.ltr [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.maxr [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.minr [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.nat_num [abbrev, in mathcomp.algebra.archimedean]
Num.Def.normr [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Def.Rneg [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.Rneg_pred [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.Rnneg [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.Rnneg_pred [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.Rnpos [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.Rnpos_pred [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.Rpos [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.Rpos_pred [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.Rreal [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.Rreal_pred [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.Def.trunc [abbrev, in mathcomp.algebra.archimedean]
Num.Def.truncn [abbrev, in mathcomp.algebra.archimedean]
Num.ExtraDef.sqrtr [abbrev, in mathcomp.algebra.numeric_hierarchy.ssrnum]
Num.floorD [abbrev, in mathcomp.algebra.archimedean]
Num.ge [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.gt [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.int [abbrev, in mathcomp.algebra.archimedean]
Num.IntegralDomain_isLeReal [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.IntegralDomain_isLeReal.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.IntegralDomain_isLeReal.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.IntegralDomain_isLtReal [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.IntegralDomain_isLtReal.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.IntegralDomain_isLtReal.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.IntegralDomain_isNumRing [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.IntegralDomain_isNumRing.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.IntegralDomain_isNumRing.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.isNumRing [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.isNumRing.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.isNumRing.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.le [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.leif [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.lt [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.lteif [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.max [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.min [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.nat [abbrev, in mathcomp.algebra.archimedean]
Num.neg [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.nneg [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.NormedZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NormedZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NormedZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NormedZmodule.Exports.normedZmodType [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NormedZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NormedZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.npos [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.NumDomain [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumDomain.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumDomain.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumDomain.Exports.numDomainType [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumDomain.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumDomain.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumDomain_bounded_isArchimedean [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_bounded_isArchimedean.axioms [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_bounded_isArchimedean.Build [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_hasFloorCeilTruncn [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_hasFloorCeilTruncn.axioms [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_hasFloorCeilTruncn.Build [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_hasTruncn [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_hasTruncn.axioms [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_hasTruncn.Build [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_isArchimedean [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_isArchimedean.Build [abbrev, in mathcomp.algebra.archimedean]
Num.NumDomain_isReal [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumDomain_isReal.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumDomain_isReal.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumField [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.NumField.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.NumField.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.NumField.Exports.numFieldType [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.NumField.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.NumField.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.NumField_isImaginary [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.NumField_isImaginary.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.NumField_isImaginary.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.NumZmod_isNumRing [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumZmod_isNumRing.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumZmod_isNumRing.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.NumZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.NumZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.NumZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.NumZmodule.Exports.numZmodType [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.NumZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.NumZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedNmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedNmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedNmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedNmodule.Exports.porderedNmodType [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedNmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedNmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedNormedZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedNormedZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedNormedZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedNormedZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedNormedZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedSemiNormedZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedSemiNormedZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedSemiNormedZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedSemiNormedZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedSemiNormedZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderedZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedZmodule.Exports.porderedZmodType [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedZmodule_hasTransCmp [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedZmodule_hasTransCmp.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderedZmodule_hasTransCmp.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderNmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderNmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderNmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderNmodule.Exports.porderNmodType [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderNmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderNmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderNormedZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderNormedZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderNormedZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderNormedZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderNormedZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderSemiNormedZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderSemiNormedZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderSemiNormedZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderSemiNormedZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderSemiNormedZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.POrderZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderZmodule.Exports.porderZmodType [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.POrderZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.pos [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.real [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.real_ceilD [abbrev, in mathcomp.algebra.archimedean]
Num.RealClosedField [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealClosedField.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealClosedField.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealClosedField.Exports.rcfType [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealClosedField.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealClosedField.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealDomain [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.RealDomain.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.RealDomain.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.RealDomain.Exports.realDomainType [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.RealDomain.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.RealDomain.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.RealField [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealField.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealField.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealField.Exports.realFieldType [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealField.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealField.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealField_isClosed [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealField_isClosed.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.RealField_isClosed.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.SemiNormedZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SemiNormedZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SemiNormedZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SemiNormedZmodule.Exports.semiNormedZmodType [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SemiNormedZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SemiNormedZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SemiNormedZmodule_isPositiveDefinite [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SemiNormedZmodule_isPositiveDefinite.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SemiNormedZmodule_isPositiveDefinite.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.sg [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.sqrt [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.SubNormedZmodule [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SubNormedZmodule.clone [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SubNormedZmodule.copy [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SubNormedZmodule.Exports.subNormedZmodType [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SubNormedZmodule.on [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.SubNormedZmodule.on_ [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Theory.ceil [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.ceil_le [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.ceil_le_int_tmp [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.char_num [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Theory.floor [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.floor_ge_int_tmp [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.floor_le_tmp [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.ge_floor [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.gt_pred_ceil [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.int_num [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.le_ceil_tmp [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.lt_succ_floor [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.mid [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.Theory.mid [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.Theory.nat_num [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.natrE [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.prod_truncK [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.real_ceil_le_int_tmp [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.real_floor_ge_int_tmp [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.real_ge_floor [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.real_gt_pred_ceil [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.real_le_ceil [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.real_lt_succ_floor [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.sqrtC [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.Theory.sqrtC [abbrev, in mathcomp.algebra.numeric_hierarchy.numfield]
Num.Theory.sum_truncK [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.trunc0 [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.trunc0Pn [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.trunc1 [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.trunc_def [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.trunc_floor [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.trunc_gt0 [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.trunc_itv [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.truncD [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.truncK [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.truncM [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.truncn [abbrev, in mathcomp.algebra.archimedean]
Num.Theory.truncX [abbrev, in mathcomp.algebra.archimedean]
Num.trunc [abbrev, in mathcomp.algebra.archimedean]
Num.Zmodule_isNormed [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Zmodule_isNormed.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Zmodule_isNormed.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Zmodule_isSemiNormed [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Zmodule_isSemiNormed.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Zmodule_isSemiNormed.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Zmodule_isSubNormed [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Zmodule_isSubNormed.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.Zmodule_isSubNormed.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.numdomain]
Num.ZmodulePositiveCone [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.ZmodulePositiveCone.axioms [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
Num.ZmodulePositiveCone.Build [abbrev, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
num_def [abbrev, in mathcomp.algebra.interval_inference]
num_itv_bound [abbrev, in mathcomp.algebra.interval_inference]
num_spec [abbrev, in mathcomp.algebra.interval_inference]
NzRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
NzRingQuotient.clone [abbrev, in mathcomp.algebra.ring_quotient]
NzRingQuotient.copy [abbrev, in mathcomp.algebra.ring_quotient]
NzRingQuotient.Exports.nzRingQuotType [abbrev, in mathcomp.algebra.ring_quotient]
NzRingQuotient.on [abbrev, in mathcomp.algebra.ring_quotient]
NzRingQuotient.on_ [abbrev, in mathcomp.algebra.ring_quotient]
NzSemiVector [abbrev, in mathcomp.algebra.vector]
NzSemiVector.clone [abbrev, in mathcomp.algebra.vector]
NzSemiVector.copy [abbrev, in mathcomp.algebra.vector]
NzSemiVector.Exports.nzSemiVectType [abbrev, in mathcomp.algebra.vector]
NzSemiVector.on [abbrev, in mathcomp.algebra.vector]
NzSemiVector.on_ [abbrev, in mathcomp.algebra.vector]
NzVector [abbrev, in mathcomp.algebra.vector]
NzVector.clone [abbrev, in mathcomp.algebra.vector]
NzVector.copy [abbrev, in mathcomp.algebra.vector]
NzVector.Exports.nzVectType [abbrev, in mathcomp.algebra.vector]
NzVector.on [abbrev, in mathcomp.algebra.vector]
NzVector.on_ [abbrev, in mathcomp.algebra.vector]