| 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 | _ | other | (24263 entries) |
| Notation 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 | _ | other | (1399 entries) |
| Module 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 | _ | other | (226 entries) |
| Variable 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 | _ | other | (3670 entries) |
| Library 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 | _ | other | (89 entries) |
| Lemma 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 | _ | other | (12297 entries) |
| Constructor 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 | _ | other | (383 entries) |
| Axiom 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 | _ | other | (45 entries) |
| Inductive 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 | _ | other | (114 entries) |
| Projection 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 | _ | other | (279 entries) |
| Section 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 | _ | other | (1169 entries) |
| Abbreviation 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 | _ | other | (742 entries) |
| Definition 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 | _ | other | (3657 entries) |
| Record 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 | _ | other | (193 entries) |
N
n [abbreviation, in mathcomp.field.fieldext]n [abbreviation, in mathcomp.field.fieldext]
n [abbreviation, in mathcomp.character.mxrepresentation]
n [abbreviation, in mathcomp.character.mxrepresentation]
n [abbreviation, in mathcomp.algebra.matrix]
n [abbreviation, in mathcomp.algebra.matrix]
n [abbreviation, in mathcomp.algebra.matrix]
n [abbreviation, in mathcomp.algebra.mxpoly]
n [abbreviation, in mathcomp.algebra.mxpoly]
n [abbreviation, in mathcomp.ssreflect.fintype]
n [abbreviation, in mathcomp.character.mxabelem]
n [abbreviation, in mathcomp.character.mxabelem]
NactionDef [section, in mathcomp.solvable.primitive_action]
NactionDef.gT [variable, in mathcomp.solvable.primitive_action]
NactionDef.n [variable, in mathcomp.solvable.primitive_action]
NactionDef.sT [variable, in mathcomp.solvable.primitive_action]
NactionDef.to [variable, in mathcomp.solvable.primitive_action]
nary_addv_subproof [lemma, in mathcomp.algebra.vector]
nary_mxsum_proof [lemma, in mathcomp.algebra.mxalgebra]
natCK [lemma, in mathcomp.field.algC]
NatConst [section, in mathcomp.ssreflect.bigop]
NatConst.A [variable, in mathcomp.ssreflect.bigop]
NatConst.I [variable, in mathcomp.ssreflect.bigop]
natnseq0P [lemma, in mathcomp.ssreflect.seq]
NatPreds [section, in mathcomp.ssreflect.prime]
NatPreds.n [variable, in mathcomp.ssreflect.prime]
NatPreds.pi [variable, in mathcomp.ssreflect.prime]
natq_div [lemma, in mathcomp.algebra.rat]
natr_negZp [lemma, in mathcomp.algebra.zmodp]
natr_Zp [lemma, in mathcomp.algebra.zmodp]
natsum_of_intK [lemma, in mathcomp.algebra.ssrint]
natsum_of_int [definition, in mathcomp.algebra.ssrint]
NatTrec [module, in mathcomp.ssreflect.ssrnat]
natTrecE [abbreviation, in mathcomp.ssreflect.ssrnat]
NatTrec.add [definition, in mathcomp.ssreflect.ssrnat]
NatTrec.addE [lemma, in mathcomp.ssreflect.ssrnat]
NatTrec.add_mulE [lemma, in mathcomp.ssreflect.ssrnat]
NatTrec.add_mul [definition, in mathcomp.ssreflect.ssrnat]
NatTrec.double [definition, in mathcomp.ssreflect.ssrnat]
NatTrec.doubleE [lemma, in mathcomp.ssreflect.ssrnat]
NatTrec.doublen [abbreviation, in mathcomp.ssreflect.ssrnat]
NatTrec.exp [definition, in mathcomp.ssreflect.ssrnat]
NatTrec.expE [lemma, in mathcomp.ssreflect.ssrnat]
NatTrec.mul [definition, in mathcomp.ssreflect.ssrnat]
NatTrec.mulE [lemma, in mathcomp.ssreflect.ssrnat]
NatTrec.mul_expE [lemma, in mathcomp.ssreflect.ssrnat]
NatTrec.mul_exp [definition, in mathcomp.ssreflect.ssrnat]
NatTrec.odd [definition, in mathcomp.ssreflect.ssrnat]
NatTrec.oddE [lemma, in mathcomp.ssreflect.ssrnat]
NatTrec.oddn [abbreviation, in mathcomp.ssreflect.ssrnat]
NatTrec.trecE [definition, in mathcomp.ssreflect.ssrnat]
_ .*2 (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]
_ ^ _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]
_ * _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]
_ + _ (nat_scope) [notation, in mathcomp.ssreflect.ssrnat]
natz [lemma, in mathcomp.algebra.ssrint]
nat_pred [definition, in mathcomp.ssreflect.prime]
nat_countMixin [definition, in mathcomp.ssreflect.choice]
nat_pickleK [lemma, in mathcomp.ssreflect.choice]
nat_choiceMixin [lemma, in mathcomp.ssreflect.choice]
nat_power_theory [lemma, in mathcomp.ssreflect.ssrnat]
nat_semi_morph [lemma, in mathcomp.ssreflect.ssrnat]
nat_semi_ring [lemma, in mathcomp.ssreflect.ssrnat]
nat_of_exp_bin [lemma, in mathcomp.ssreflect.ssrnat]
nat_of_mul_bin [lemma, in mathcomp.ssreflect.ssrnat]
nat_of_add_bin [lemma, in mathcomp.ssreflect.ssrnat]
nat_of_mul_pos [lemma, in mathcomp.ssreflect.ssrnat]
nat_of_add_pos [lemma, in mathcomp.ssreflect.ssrnat]
nat_of_succ_pos [lemma, in mathcomp.ssreflect.ssrnat]
nat_of_binK [lemma, in mathcomp.ssreflect.ssrnat]
nat_of_pos [definition, in mathcomp.ssreflect.ssrnat]
nat_AGM2 [lemma, in mathcomp.ssreflect.ssrnat]
nat_Cauchy [lemma, in mathcomp.ssreflect.ssrnat]
nat_irrelevance [lemma, in mathcomp.ssreflect.ssrnat]
nclasses_isog [lemma, in mathcomp.fingroup.morphism]
nclasses_injm [lemma, in mathcomp.fingroup.morphism]
ncons [definition, in mathcomp.ssreflect.seq]
nconsK [lemma, in mathcomp.ssreflect.seq]
ncprod [definition, in mathcomp.solvable.center]
ncprodS [lemma, in mathcomp.solvable.center]
ncprod_key [lemma, in mathcomp.solvable.center]
ncprod_def [definition, in mathcomp.solvable.center]
ncprod0 [lemma, in mathcomp.solvable.center]
ncprod1 [lemma, in mathcomp.solvable.center]
ncycles_mul_tperm [lemma, in mathcomp.fingroup.perm]
nderivn [definition, in mathcomp.algebra.poly]
nderivnB [lemma, in mathcomp.algebra.poly]
nderivnC [lemma, in mathcomp.algebra.poly]
nderivnD [lemma, in mathcomp.algebra.poly]
nderivnMn [lemma, in mathcomp.algebra.poly]
nderivnMNn [lemma, in mathcomp.algebra.poly]
nderivnMXaddC [lemma, in mathcomp.algebra.poly]
nderivnN [lemma, in mathcomp.algebra.poly]
nderivnXn [lemma, in mathcomp.algebra.poly]
nderivnZ [lemma, in mathcomp.algebra.poly]
nderivn_map [lemma, in mathcomp.algebra.poly]
nderivn_poly0 [lemma, in mathcomp.algebra.poly]
nderivn_is_linear [lemma, in mathcomp.algebra.poly]
nderivn_def [lemma, in mathcomp.algebra.poly]
nderivn0 [lemma, in mathcomp.algebra.poly]
nderivn1 [lemma, in mathcomp.algebra.poly]
nderiv_taylor_wide [lemma, in mathcomp.algebra.poly]
nderiv_taylor [lemma, in mathcomp.algebra.poly]
ndirr [definition, in mathcomp.character.vcharacter]
ndirrK [lemma, in mathcomp.character.vcharacter]
ndirr_inj [lemma, in mathcomp.character.vcharacter]
ndirr_diff [lemma, in mathcomp.character.vcharacter]
ndir_s0p [lemma, in mathcomp.solvable.burnside_app]
negb_exists_in [lemma, in mathcomp.ssreflect.fintype]
negb_exists [lemma, in mathcomp.ssreflect.fintype]
negb_forall_in [lemma, in mathcomp.ssreflect.fintype]
negb_forall [lemma, in mathcomp.ssreflect.fintype]
negb_eqb [lemma, in mathcomp.ssreflect.eqtype]
negb_add [lemma, in mathcomp.ssreflect.eqtype]
negn [definition, in mathcomp.ssreflect.prime]
negnK [lemma, in mathcomp.ssreflect.prime]
Negz [constructor, in mathcomp.algebra.ssrint]
NegzE [lemma, in mathcomp.algebra.ssrint]
nElem [definition, in mathcomp.solvable.abelian]
nElemI [lemma, in mathcomp.solvable.abelian]
nElemP [lemma, in mathcomp.solvable.abelian]
nElemS [lemma, in mathcomp.solvable.abelian]
nElem0 [lemma, in mathcomp.solvable.abelian]
nElem1P [lemma, in mathcomp.solvable.abelian]
NeqNotEq [constructor, in mathcomp.ssreflect.eqtype]
neq_lift [lemma, in mathcomp.ssreflect.fintype]
neq_bump [lemma, in mathcomp.ssreflect.fintype]
neq_ltn [lemma, in mathcomp.ssreflect.ssrnat]
neq0CG [lemma, in mathcomp.character.classfun]
neq0CiG [lemma, in mathcomp.character.classfun]
neq0_has_constt [lemma, in mathcomp.character.character]
neq0_lt0n [lemma, in mathcomp.ssreflect.ssrnat]
NewType [definition, in mathcomp.ssreflect.eqtype]
nexpIrz [lemma, in mathcomp.algebra.ssrint]
next [definition, in mathcomp.ssreflect.path]
nextE [lemma, in mathcomp.ssreflect.path]
next_map [lemma, in mathcomp.ssreflect.path]
next_rev [lemma, in mathcomp.ssreflect.path]
next_rotr [lemma, in mathcomp.ssreflect.path]
next_rot [lemma, in mathcomp.ssreflect.path]
next_prev [lemma, in mathcomp.ssreflect.path]
next_cycle [lemma, in mathcomp.ssreflect.path]
next_nth [lemma, in mathcomp.ssreflect.path]
next_at [definition, in mathcomp.ssreflect.path]
nG [abbreviation, in mathcomp.character.mxrepresentation]
nG [abbreviation, in mathcomp.character.mxrepresentation]
nhomo_inj_lt_in [lemma, in mathcomp.ssreflect.ssrnat]
nhomo_inj_lt [lemma, in mathcomp.ssreflect.ssrnat]
Nil [abbreviation, in mathcomp.ssreflect.seq]
nilP [lemma, in mathcomp.ssreflect.seq]
nilp [definition, in mathcomp.ssreflect.seq]
NilPGroups [section, in mathcomp.solvable.sylow]
NilPGroups.gT [variable, in mathcomp.solvable.sylow]
NilPGroups.p [variable, in mathcomp.solvable.sylow]
nilpotent [definition, in mathcomp.solvable.nilpotent]
Nilpotent [section, in mathcomp.solvable.sylow]
nilpotent [library]
NilpotentProps [section, in mathcomp.solvable.nilpotent]
NilpotentProps.gT [variable, in mathcomp.solvable.nilpotent]
nilpotentS [lemma, in mathcomp.solvable.nilpotent]
nilpotent_Fitting [lemma, in mathcomp.solvable.maximal]
nilpotent_sol [lemma, in mathcomp.solvable.nilpotent]
nilpotent_subnormal [lemma, in mathcomp.solvable.nilpotent]
nilpotent_proper_norm [lemma, in mathcomp.solvable.nilpotent]
nilpotent_sub_norm [lemma, in mathcomp.solvable.nilpotent]
nilpotent_class [lemma, in mathcomp.solvable.nilpotent]
nilpotent_pcoreC [lemma, in mathcomp.solvable.sylow]
nilpotent_pcore_Hall [lemma, in mathcomp.solvable.sylow]
nilpotent_Hall_pcore [lemma, in mathcomp.solvable.sylow]
nilpotent_maxp_normal [lemma, in mathcomp.solvable.sylow]
Nilpotent.gT [variable, in mathcomp.solvable.sylow]
nilpotent1 [lemma, in mathcomp.solvable.nilpotent]
nil_basis [lemma, in mathcomp.algebra.vector]
nil_free [lemma, in mathcomp.algebra.vector]
nil_poly [lemma, in mathcomp.algebra.poly]
nil_class_quotient_center [lemma, in mathcomp.solvable.nilpotent]
nil_class_injm [lemma, in mathcomp.solvable.nilpotent]
nil_class_morphim [lemma, in mathcomp.solvable.nilpotent]
nil_class_ucn [lemma, in mathcomp.solvable.nilpotent]
nil_class1 [lemma, in mathcomp.solvable.nilpotent]
nil_class0 [lemma, in mathcomp.solvable.nilpotent]
nil_comm_properr [lemma, in mathcomp.solvable.nilpotent]
nil_comm_properl [lemma, in mathcomp.solvable.nilpotent]
nil_class [definition, in mathcomp.solvable.nilpotent]
nil_Zgroup_cyclic [lemma, in mathcomp.solvable.sylow]
nil_class_pgroup [lemma, in mathcomp.solvable.sylow]
nil_class3 [lemma, in mathcomp.solvable.sylow]
nil_class2 [lemma, in mathcomp.solvable.sylow]
Nirr [abbreviation, in mathcomp.character.character]
NirrE [lemma, in mathcomp.character.character]
nmulrn [lemma, in mathcomp.algebra.ssrint]
nmulrz_rle0 [lemma, in mathcomp.algebra.ssrint]
nmulrz_rge0 [lemma, in mathcomp.algebra.ssrint]
nmulrz_rlt0 [lemma, in mathcomp.algebra.ssrint]
nmulrz_rgt0 [lemma, in mathcomp.algebra.ssrint]
nmulrz_lle0 [lemma, in mathcomp.algebra.ssrint]
nmulrz_lge0 [lemma, in mathcomp.algebra.ssrint]
nmulrz_llt0 [lemma, in mathcomp.algebra.ssrint]
nmulrz_lgt0 [lemma, in mathcomp.algebra.ssrint]
nonconform_mx [lemma, in mathcomp.algebra.matrix]
nonlinear_irr_vanish [lemma, in mathcomp.character.integral_char]
NonPropType [module, in mathcomp.ssreflect.ssreflect]
NonPropType.call [definition, in mathcomp.ssreflect.ssreflect]
NonPropType.Call [constructor, in mathcomp.ssreflect.ssreflect]
NonPropType.callee [projection, in mathcomp.ssreflect.ssreflect]
NonPropType.call_of [record, in mathcomp.ssreflect.ssreflect]
NonPropType.check [definition, in mathcomp.ssreflect.ssreflect]
NonPropType.Check [constructor, in mathcomp.ssreflect.ssreflect]
NonPropType.condition [projection, in mathcomp.ssreflect.ssreflect]
NonPropType.Exports [module, in mathcomp.ssreflect.ssreflect]
NonPropType.Exports.nonPropType [abbreviation, in mathcomp.ssreflect.ssreflect]
NonPropType.Exports.notProp [abbreviation, in mathcomp.ssreflect.ssreflect]
NonPropType.frame [projection, in mathcomp.ssreflect.ssreflect]
NonPropType.maybeProp [definition, in mathcomp.ssreflect.ssreflect]
NonPropType.result [projection, in mathcomp.ssreflect.ssreflect]
NonPropType.test [projection, in mathcomp.ssreflect.ssreflect]
NonPropType.Test [constructor, in mathcomp.ssreflect.ssreflect]
NonPropType.test_negative [definition, in mathcomp.ssreflect.ssreflect]
NonPropType.test_Prop [definition, in mathcomp.ssreflect.ssreflect]
NonPropType.test_of [record, in mathcomp.ssreflect.ssreflect]
NonPropType.type [record, in mathcomp.ssreflect.ssreflect]
nontrivial_gacent_pgroup [lemma, in mathcomp.solvable.sylow]
nonzero1fx [lemma, in mathcomp.field.fieldext]
nonzero1q [lemma, in mathcomp.algebra.rat]
Nopick [constructor, in mathcomp.ssreflect.fintype]
normal [definition, in mathcomp.fingroup.fingroup]
normalD1 [lemma, in mathcomp.fingroup.fingroup]
normalField [definition, in mathcomp.field.galois]
normalFieldf [lemma, in mathcomp.field.galois]
normalFieldP [lemma, in mathcomp.field.galois]
normalFieldS [lemma, in mathcomp.field.galois]
normalField_isog [lemma, in mathcomp.field.galois]
normalField_isom [lemma, in mathcomp.field.galois]
normalField_img [lemma, in mathcomp.field.galois]
normalField_normal [lemma, in mathcomp.field.galois]
normalField_ker [lemma, in mathcomp.field.galois]
normalField_castM [lemma, in mathcomp.field.galois]
normalField_cast_eq [lemma, in mathcomp.field.galois]
normalField_cast [definition, in mathcomp.field.galois]
normalField_galois [lemma, in mathcomp.field.galois]
normalField_factors [lemma, in mathcomp.field.galois]
normalField_root_minPoly [lemma, in mathcomp.field.galois]
normalField_kAut [lemma, in mathcomp.field.galois]
normalG [lemma, in mathcomp.fingroup.fingroup]
normalGI [lemma, in mathcomp.fingroup.fingroup]
NormalHall [section, in mathcomp.solvable.pgroup]
NormalHall.gT [variable, in mathcomp.solvable.pgroup]
NormalHall.pi [variable, in mathcomp.solvable.pgroup]
normalI [lemma, in mathcomp.fingroup.fingroup]
normalised [definition, in mathcomp.fingroup.fingroup]
Normaliser [section, in mathcomp.fingroup.fingroup]
normaliser [definition, in mathcomp.fingroup.fingroup]
Normaliser.gT [variable, in mathcomp.fingroup.fingroup]
Normaliser.norm_trans.nCA [variable, in mathcomp.fingroup.fingroup]
Normaliser.norm_trans.nBA [variable, in mathcomp.fingroup.fingroup]
Normaliser.norm_trans.D [variable, in mathcomp.fingroup.fingroup]
Normaliser.norm_trans.C [variable, in mathcomp.fingroup.fingroup]
Normaliser.norm_trans.B [variable, in mathcomp.fingroup.fingroup]
Normaliser.norm_trans.A [variable, in mathcomp.fingroup.fingroup]
Normaliser.norm_trans [section, in mathcomp.fingroup.fingroup]
Normaliser.SubAbelian [section, in mathcomp.fingroup.fingroup]
Normaliser.SubAbelian.A [variable, in mathcomp.fingroup.fingroup]
Normaliser.SubAbelian.B [variable, in mathcomp.fingroup.fingroup]
Normaliser.SubAbelian.C [variable, in mathcomp.fingroup.fingroup]
Normaliser.SubAbelian.cAA [variable, in mathcomp.fingroup.fingroup]
normalJ [lemma, in mathcomp.fingroup.fingroup]
normalM [lemma, in mathcomp.fingroup.fingroup]
normalP [lemma, in mathcomp.fingroup.fingroup]
normalS [lemma, in mathcomp.fingroup.fingroup]
normalSG [lemma, in mathcomp.fingroup.fingroup]
normalY [lemma, in mathcomp.fingroup.fingroup]
normalYl [lemma, in mathcomp.fingroup.fingroup]
normalYr [lemma, in mathcomp.fingroup.fingroup]
normal_fixedField_galois [lemma, in mathcomp.field.galois]
normal_field_splitting [lemma, in mathcomp.field.galois]
normal_Hall_pcore [lemma, in mathcomp.solvable.pgroup]
normal_max_pgroup_Hall [lemma, in mathcomp.solvable.pgroup]
normal_sub_max_pgroup [lemma, in mathcomp.solvable.pgroup]
normal_cosetpre [lemma, in mathcomp.fingroup.quotient]
normal_rfix_mx_module [lemma, in mathcomp.character.mxrepresentation]
normal_rank1_structure [lemma, in mathcomp.solvable.extremal]
normal_Inertia [lemma, in mathcomp.character.inertia]
normal_inertia [lemma, in mathcomp.character.inertia]
normal_subnormal [lemma, in mathcomp.solvable.gseries]
normal_subnorm [lemma, in mathcomp.fingroup.fingroup]
normal_refl [lemma, in mathcomp.fingroup.fingroup]
normal_norm [lemma, in mathcomp.fingroup.fingroup]
normal_sub [lemma, in mathcomp.fingroup.fingroup]
normal_pgroup [lemma, in mathcomp.solvable.sylow]
normal_sylowP [lemma, in mathcomp.solvable.sylow]
normal1 [lemma, in mathcomp.fingroup.fingroup]
normC [lemma, in mathcomp.fingroup.fingroup]
normCs [lemma, in mathcomp.fingroup.fingroup]
normC_lin_char [lemma, in mathcomp.character.character]
normD1 [lemma, in mathcomp.fingroup.fingroup]
normedTI [definition, in mathcomp.solvable.frobenius]
normedTI_J [lemma, in mathcomp.solvable.frobenius]
normedTI_S [lemma, in mathcomp.solvable.frobenius]
normedTI_memJ_P [lemma, in mathcomp.solvable.frobenius]
normedTI_P [lemma, in mathcomp.solvable.frobenius]
normG [lemma, in mathcomp.fingroup.fingroup]
NormInt [section, in mathcomp.algebra.ssrint]
NormInt.R [variable, in mathcomp.algebra.ssrint]
normJ [lemma, in mathcomp.fingroup.fingroup]
normP [lemma, in mathcomp.fingroup.fingroup]
normq [definition, in mathcomp.algebra.rat]
normrMz [lemma, in mathcomp.algebra.ssrint]
normr_num_div [lemma, in mathcomp.algebra.rat]
normr_denq [lemma, in mathcomp.algebra.rat]
normr_sg [lemma, in mathcomp.algebra.ssrint]
normr_sgz [lemma, in mathcomp.algebra.ssrint]
normsD [lemma, in mathcomp.fingroup.fingroup]
normsD1 [lemma, in mathcomp.fingroup.fingroup]
normsG [lemma, in mathcomp.fingroup.fingroup]
normsGI [lemma, in mathcomp.fingroup.fingroup]
normsI [lemma, in mathcomp.fingroup.fingroup]
normsIG [lemma, in mathcomp.fingroup.fingroup]
normsIs [lemma, in mathcomp.fingroup.fingroup]
normsM [lemma, in mathcomp.fingroup.fingroup]
normsP [lemma, in mathcomp.fingroup.fingroup]
normsR [lemma, in mathcomp.fingroup.fingroup]
normsRl [lemma, in mathcomp.solvable.commutator]
normsRr [lemma, in mathcomp.solvable.commutator]
normsU [lemma, in mathcomp.fingroup.fingroup]
normsY [lemma, in mathcomp.fingroup.fingroup]
norms_cent [lemma, in mathcomp.fingroup.fingroup]
norms_bigcup [lemma, in mathcomp.fingroup.fingroup]
norms_bigcap [lemma, in mathcomp.fingroup.fingroup]
norms_class_support [lemma, in mathcomp.fingroup.fingroup]
norms_norm [lemma, in mathcomp.fingroup.fingroup]
norms_gen [lemma, in mathcomp.fingroup.fingroup]
norms_cycle [lemma, in mathcomp.fingroup.fingroup]
norms1 [lemma, in mathcomp.fingroup.fingroup]
normT [lemma, in mathcomp.fingroup.fingroup]
norm_ratN [lemma, in mathcomp.algebra.rat]
norm_conj_cent [lemma, in mathcomp.solvable.hall]
norm_Cint_ge1 [lemma, in mathcomp.field.algC]
norm_Cnat [lemma, in mathcomp.field.algC]
norm_sub_max_pgroup [lemma, in mathcomp.solvable.pgroup]
norm_quotient_pre [lemma, in mathcomp.fingroup.quotient]
norm_sub_rstabs_rfix_mx [lemma, in mathcomp.character.mxrepresentation]
norm_conj_autE [lemma, in mathcomp.fingroup.automorphism]
norm_conj_isom [lemma, in mathcomp.fingroup.automorphism]
norm_conjg_im [lemma, in mathcomp.fingroup.automorphism]
norm_Inertia [lemma, in mathcomp.character.inertia]
norm_inertia [lemma, in mathcomp.character.inertia]
norm_normalI [lemma, in mathcomp.fingroup.fingroup]
norm_gen [lemma, in mathcomp.fingroup.fingroup]
norm_conj_norm [lemma, in mathcomp.fingroup.fingroup]
norm_rlcoset [lemma, in mathcomp.fingroup.fingroup]
norm_joinEr [lemma, in mathcomp.fingroup.fingroup]
norm_joinEl [lemma, in mathcomp.fingroup.fingroup]
norm1 [lemma, in mathcomp.fingroup.fingroup]
Norm1vchar [section, in mathcomp.character.vcharacter]
Norm1vchar.G [variable, in mathcomp.character.vcharacter]
Norm1vchar.gT [variable, in mathcomp.character.vcharacter]
NotExtremal [constructor, in mathcomp.solvable.extremal]
notin_iter [lemma, in mathcomp.ssreflect.finset]
not_simple_Alt_4 [lemma, in mathcomp.solvable.alt]
not_isog_Dn_DnQ [lemma, in mathcomp.solvable.extraspecial]
not_asubv0 [lemma, in mathcomp.field.falgebra]
nseq [definition, in mathcomp.ssreflect.seq]
nseqP [lemma, in mathcomp.ssreflect.seq]
nseq_tupleP [lemma, in mathcomp.ssreflect.tuple]
nseq_addn [lemma, in mathcomp.ssreflect.seq]
nth [abbreviation, in mathcomp.ssreflect.seq]
nth [definition, in mathcomp.ssreflect.seq]
nthK [lemma, in mathcomp.ssreflect.seq]
nthP [lemma, in mathcomp.ssreflect.seq]
NthTheory [section, in mathcomp.ssreflect.seq]
NthTheory.T [variable, in mathcomp.ssreflect.seq]
nth_traject [lemma, in mathcomp.ssreflect.path]
nth_mktuple [lemma, in mathcomp.ssreflect.tuple]
nth_flatten [lemma, in mathcomp.ssreflect.seq]
nth_shape [lemma, in mathcomp.ssreflect.seq]
nth_reshape [lemma, in mathcomp.ssreflect.seq]
nth_zip_cond [lemma, in mathcomp.ssreflect.seq]
nth_zip [lemma, in mathcomp.ssreflect.seq]
nth_scanl [lemma, in mathcomp.ssreflect.seq]
nth_pairmap [lemma, in mathcomp.ssreflect.seq]
nth_mkseq [lemma, in mathcomp.ssreflect.seq]
nth_iota [lemma, in mathcomp.ssreflect.seq]
nth_index_map [lemma, in mathcomp.ssreflect.seq]
nth_map [lemma, in mathcomp.ssreflect.seq]
nth_incr_nth [lemma, in mathcomp.ssreflect.seq]
nth_uniq [lemma, in mathcomp.ssreflect.seq]
nth_index [lemma, in mathcomp.ssreflect.seq]
nth_rev [lemma, in mathcomp.ssreflect.seq]
nth_take [lemma, in mathcomp.ssreflect.seq]
nth_drop [lemma, in mathcomp.ssreflect.seq]
nth_find [lemma, in mathcomp.ssreflect.seq]
nth_set_nth [lemma, in mathcomp.ssreflect.seq]
nth_nseq [lemma, in mathcomp.ssreflect.seq]
nth_ncons [lemma, in mathcomp.ssreflect.seq]
nth_rcons_default [lemma, in mathcomp.ssreflect.seq]
nth_rcons [lemma, in mathcomp.ssreflect.seq]
nth_cat [lemma, in mathcomp.ssreflect.seq]
nth_behead [lemma, in mathcomp.ssreflect.seq]
nth_last [lemma, in mathcomp.ssreflect.seq]
nth_nil [lemma, in mathcomp.ssreflect.seq]
nth_default [lemma, in mathcomp.ssreflect.seq]
nth_enum_rank [lemma, in mathcomp.ssreflect.fintype]
nth_enum_rank_in [lemma, in mathcomp.ssreflect.fintype]
nth_codom [lemma, in mathcomp.ssreflect.fintype]
nth_image [lemma, in mathcomp.ssreflect.fintype]
nth_ord_enum [lemma, in mathcomp.ssreflect.fintype]
nth_enum_ord [lemma, in mathcomp.ssreflect.fintype]
nth_fgraph_ord [lemma, in mathcomp.ssreflect.finfun]
nth0 [lemma, in mathcomp.ssreflect.seq]
ntransitive [definition, in mathcomp.solvable.primitive_action]
NTransitive [section, in mathcomp.solvable.primitive_action]
ntransitive_primitive [lemma, in mathcomp.solvable.primitive_action]
ntransitive_weak [lemma, in mathcomp.solvable.primitive_action]
NTransitive.A [variable, in mathcomp.solvable.primitive_action]
NTransitive.gT [variable, in mathcomp.solvable.primitive_action]
NTransitive.n [variable, in mathcomp.solvable.primitive_action]
NTransitive.S [variable, in mathcomp.solvable.primitive_action]
NTransitive.sT [variable, in mathcomp.solvable.primitive_action]
NTransitive.to [variable, in mathcomp.solvable.primitive_action]
ntransitive0 [lemma, in mathcomp.solvable.primitive_action]
ntransitive1 [lemma, in mathcomp.solvable.primitive_action]
NTransitveProp [section, in mathcomp.solvable.primitive_action]
NTransitveProp.G [variable, in mathcomp.solvable.primitive_action]
NTransitveProp.gT [variable, in mathcomp.solvable.primitive_action]
NTransitveProp.S [variable, in mathcomp.solvable.primitive_action]
NTransitveProp.sT [variable, in mathcomp.solvable.primitive_action]
NTransitveProp.to [variable, in mathcomp.solvable.primitive_action]
NTransitveProp1 [section, in mathcomp.solvable.primitive_action]
NTransitveProp1.G [variable, in mathcomp.solvable.primitive_action]
NTransitveProp1.gT [variable, in mathcomp.solvable.primitive_action]
NTransitveProp1.S [variable, in mathcomp.solvable.primitive_action]
NTransitveProp1.sT [variable, in mathcomp.solvable.primitive_action]
NTransitveProp1.to [variable, in mathcomp.solvable.primitive_action]
nt_pnElem [lemma, in mathcomp.solvable.abelian]
nt_prime_order [lemma, in mathcomp.solvable.cyclic]
nt_gen_prime [lemma, in mathcomp.solvable.cyclic]
Num [constructor, in mathcomp.ssreflect.ssrnat]
Num [module, in mathcomp.algebra.ssrnum]
number [record, in mathcomp.ssreflect.ssrnat]
NumberInterpretation [section, in mathcomp.ssreflect.ssrnat]
NumberInterpretation.Trec [section, in mathcomp.ssreflect.ssrnat]
number_eqMixin [definition, in mathcomp.ssreflect.ssrnat]
numden_Ratio [definition, in mathcomp.algebra.fraction]
numer_Ratio [lemma, in mathcomp.algebra.fraction]
NumFactor [definition, in mathcomp.ssreflect.prime]
NumFieldProj [section, in mathcomp.field.algnum]
NumFieldProj.Qn [variable, in mathcomp.field.algnum]
NumFieldProj.QnC [variable, in mathcomp.field.algnum]
NumLRmorphism [definition, in mathcomp.field.algnum]
numq [definition, in mathcomp.algebra.rat]
numqE [lemma, in mathcomp.algebra.rat]
numqK [lemma, in mathcomp.algebra.rat]
numqN [lemma, in mathcomp.algebra.rat]
numq_lt0 [lemma, in mathcomp.algebra.rat]
numq_gt0 [lemma, in mathcomp.algebra.rat]
numq_le0 [lemma, in mathcomp.algebra.rat]
numq_ge0 [lemma, in mathcomp.algebra.rat]
numq_div_lt0 [lemma, in mathcomp.algebra.rat]
numq_sign_mul [lemma, in mathcomp.algebra.rat]
numq_int [lemma, in mathcomp.algebra.rat]
numq_eq0 [lemma, in mathcomp.algebra.rat]
num_field_proj [lemma, in mathcomp.field.algnum]
num_field_exists [lemma, in mathcomp.field.algnum]
Num.ArchimedeanField [module, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.base [projection, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.choiceType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.class [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.Class [constructor, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.ClassDef [section, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.ClassDef.cT [variable, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.ClassDef.T [variable, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.ClassDef.xT [variable, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.class_of [record, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.clone [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.comRingType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.comUnitRingType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.eqType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.Exports [module, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.Exports.ArchiFieldType [abbreviation, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.Exports.archiFieldType [abbreviation, in mathcomp.algebra.ssrnum]
[ archiFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ archiFieldType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.fieldType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.idomainType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.numDomainType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.numFieldType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.pack [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.Pack [constructor, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.realDomainType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.realFieldType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.ringType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.sort [projection, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.type [record, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.unitRingType [definition, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.xclass [abbreviation, in mathcomp.algebra.ssrnum]
Num.ArchimedeanField.zmodType [definition, in mathcomp.algebra.ssrnum]
Num.archimedean_axiom [definition, in mathcomp.algebra.ssrnum]
Num.bound [abbreviation, in mathcomp.algebra.ssrnum]
Num.ClosedField [module, in mathcomp.algebra.ssrnum]
Num.ClosedField.base [projection, in mathcomp.algebra.ssrnum]
Num.ClosedField.base2 [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.choiceType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.class [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.Class [constructor, in mathcomp.algebra.ssrnum]
Num.ClosedField.ClassDef [section, in mathcomp.algebra.ssrnum]
Num.ClosedField.ClassDef.cT [variable, in mathcomp.algebra.ssrnum]
Num.ClosedField.ClassDef.T [variable, in mathcomp.algebra.ssrnum]
Num.ClosedField.ClassDef.xT [variable, in mathcomp.algebra.ssrnum]
Num.ClosedField.class_of [record, in mathcomp.algebra.ssrnum]
Num.ClosedField.clone [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.closedFieldType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.comRingType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.comUnitRingType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.conj_mixin [projection, in mathcomp.algebra.ssrnum]
Num.ClosedField.conj_op [projection, in mathcomp.algebra.ssrnum]
Num.ClosedField.decFieldType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.eqType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.Exports [module, in mathcomp.algebra.ssrnum]
Num.ClosedField.Exports.NumClosedFieldType [abbreviation, in mathcomp.algebra.ssrnum]
Num.ClosedField.Exports.numClosedFieldType [abbreviation, in mathcomp.algebra.ssrnum]
[ numClosedFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ numClosedFieldType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
Num.ClosedField.fieldType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.idomainType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.imaginary [projection, in mathcomp.algebra.ssrnum]
Num.ClosedField.ImaginaryMixin [constructor, in mathcomp.algebra.ssrnum]
Num.ClosedField.imaginary_mixin_of [record, in mathcomp.algebra.ssrnum]
Num.ClosedField.join_numFieldType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.join_numDomainType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.join_dec_numFieldType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.join_dec_numDomainType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.mixin [projection, in mathcomp.algebra.ssrnum]
Num.ClosedField.numDomainType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.numFieldType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.pack [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.Pack [constructor, in mathcomp.algebra.ssrnum]
Num.ClosedField.ringType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.sort [projection, in mathcomp.algebra.ssrnum]
Num.ClosedField.type [record, in mathcomp.algebra.ssrnum]
Num.ClosedField.unitRingType [definition, in mathcomp.algebra.ssrnum]
Num.ClosedField.xclass [abbreviation, in mathcomp.algebra.ssrnum]
Num.ClosedField.zmodType [definition, in mathcomp.algebra.ssrnum]
Num.Def [module, in mathcomp.algebra.ssrnum]
Num.Def.Def [section, in mathcomp.algebra.ssrnum]
_ < _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ <= _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
Num.Def.ger [definition, in mathcomp.algebra.ssrnum]
Num.Def.gtr [definition, in mathcomp.algebra.ssrnum]
Num.Def.ler [definition, in mathcomp.algebra.ssrnum]
Num.Def.lerif [definition, in mathcomp.algebra.ssrnum]
Num.Def.ltr [definition, in mathcomp.algebra.ssrnum]
Num.Def.maxr [definition, in mathcomp.algebra.ssrnum]
Num.Def.minr [definition, in mathcomp.algebra.ssrnum]
Num.Def.normr [definition, in mathcomp.algebra.ssrnum]
Num.Def.Rneg [definition, in mathcomp.algebra.ssrnum]
Num.Def.Rnneg [definition, in mathcomp.algebra.ssrnum]
Num.Def.Rpos [definition, in mathcomp.algebra.ssrnum]
Num.Def.Rreal [definition, in mathcomp.algebra.ssrnum]
Num.Def.sgr [definition, in mathcomp.algebra.ssrnum]
Num.ExtensionAxioms [section, in mathcomp.algebra.ssrnum]
Num.ExtensionAxioms.R [variable, in mathcomp.algebra.ssrnum]
Num.ExtraDef [module, in mathcomp.algebra.ssrnum]
Num.ExtraDef.archi_bound [definition, in mathcomp.algebra.ssrnum]
Num.ExtraDef.sqrtr [definition, in mathcomp.algebra.ssrnum]
Num.ge [abbreviation, in mathcomp.algebra.ssrnum]
Num.gt [abbreviation, in mathcomp.algebra.ssrnum]
Num.Internals [module, in mathcomp.algebra.ssrnum]
Num.Internals.addr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.addr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.archi_bound_subproof [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.Domain [section, in mathcomp.algebra.ssrnum]
Num.Internals.Domain.R [variable, in mathcomp.algebra.ssrnum]
Num.Internals.ger_leVge [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.ger0_def [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.lerr [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.ler_def [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.ler_norm_add [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.ler01 [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.le0r [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.ltrW [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.ltr_def [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.ltr01 [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.nnegrE [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.nneg_addr_closed [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.nneg_divr_closed [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.normrM [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.normr0_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.num_real [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.oppr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.pmulr_rgt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.poly_ivt [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.posrE [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.pos_divr_closed [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.RealClosed [section, in mathcomp.algebra.ssrnum]
Num.Internals.RealClosed.R [variable, in mathcomp.algebra.ssrnum]
Num.Internals.realE [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.real_divr_closed [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.real_addr_closed [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.real_oppr_closed [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.sqrtr_subproof [lemma, in mathcomp.algebra.ssrnum]
Num.Internals.subr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Keys [module, in mathcomp.algebra.ssrnum]
Num.Keys.Keys [section, in mathcomp.algebra.ssrnum]
Num.Keys.Keys.R [variable, in mathcomp.algebra.ssrnum]
Num.Keys.ler_of_leif [definition, in mathcomp.algebra.ssrnum]
Num.Keys.Rneg_keyed [definition, in mathcomp.algebra.ssrnum]
Num.Keys.Rneg_key [lemma, in mathcomp.algebra.ssrnum]
Num.Keys.Rnneg_keyed [definition, in mathcomp.algebra.ssrnum]
Num.Keys.Rnneg_key [lemma, in mathcomp.algebra.ssrnum]
Num.Keys.Rpos_keyed [definition, in mathcomp.algebra.ssrnum]
Num.Keys.Rpos_key [lemma, in mathcomp.algebra.ssrnum]
Num.Keys.Rreal_keyed [definition, in mathcomp.algebra.ssrnum]
Num.Keys.Rreal_key [lemma, in mathcomp.algebra.ssrnum]
Num.le [abbreviation, in mathcomp.algebra.ssrnum]
Num.le_op [projection, in mathcomp.algebra.ssrnum]
Num.lt [abbreviation, in mathcomp.algebra.ssrnum]
Num.lt_op [projection, in mathcomp.algebra.ssrnum]
Num.max [abbreviation, in mathcomp.algebra.ssrnum]
Num.min [abbreviation, in mathcomp.algebra.ssrnum]
Num.Mixin [constructor, in mathcomp.algebra.ssrnum]
Num.mixin_of [record, in mathcomp.algebra.ssrnum]
Num.neg [abbreviation, in mathcomp.algebra.ssrnum]
Num.nneg [abbreviation, in mathcomp.algebra.ssrnum]
Num.norm [abbreviation, in mathcomp.algebra.ssrnum]
Num.norm_op [projection, in mathcomp.algebra.ssrnum]
Num.NumDomain [module, in mathcomp.algebra.ssrnum]
Num.NumDomain.base [projection, in mathcomp.algebra.ssrnum]
Num.NumDomain.choiceType [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.class [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.Class [constructor, in mathcomp.algebra.ssrnum]
Num.NumDomain.ClassDef [section, in mathcomp.algebra.ssrnum]
Num.NumDomain.ClassDef.cT [variable, in mathcomp.algebra.ssrnum]
Num.NumDomain.ClassDef.T [variable, in mathcomp.algebra.ssrnum]
Num.NumDomain.ClassDef.xT [variable, in mathcomp.algebra.ssrnum]
Num.NumDomain.class_of [record, in mathcomp.algebra.ssrnum]
Num.NumDomain.clone [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.comRingType [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.comUnitRingType [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.eqType [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.Exports [module, in mathcomp.algebra.ssrnum]
Num.NumDomain.Exports.NumDomainType [abbreviation, in mathcomp.algebra.ssrnum]
Num.NumDomain.Exports.numDomainType [abbreviation, in mathcomp.algebra.ssrnum]
Num.NumDomain.Exports.NumMixin [abbreviation, in mathcomp.algebra.ssrnum]
[ numDomainType of _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ numDomainType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
Num.NumDomain.idomainType [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.mixin [projection, in mathcomp.algebra.ssrnum]
Num.NumDomain.pack [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.Pack [constructor, in mathcomp.algebra.ssrnum]
Num.NumDomain.ringType [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.sort [projection, in mathcomp.algebra.ssrnum]
Num.NumDomain.type [record, in mathcomp.algebra.ssrnum]
Num.NumDomain.unitRingType [definition, in mathcomp.algebra.ssrnum]
Num.NumDomain.xclass [abbreviation, in mathcomp.algebra.ssrnum]
Num.NumDomain.zmodType [definition, in mathcomp.algebra.ssrnum]
Num.NumField [module, in mathcomp.algebra.ssrnum]
Num.NumField.base [projection, in mathcomp.algebra.ssrnum]
Num.NumField.base2 [definition, in mathcomp.algebra.ssrnum]
Num.NumField.choiceType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.class [definition, in mathcomp.algebra.ssrnum]
Num.NumField.Class [constructor, in mathcomp.algebra.ssrnum]
Num.NumField.ClassDef [section, in mathcomp.algebra.ssrnum]
Num.NumField.ClassDef.cT [variable, in mathcomp.algebra.ssrnum]
Num.NumField.ClassDef.T [variable, in mathcomp.algebra.ssrnum]
Num.NumField.ClassDef.xT [variable, in mathcomp.algebra.ssrnum]
Num.NumField.class_of [record, in mathcomp.algebra.ssrnum]
Num.NumField.comRingType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.comUnitRingType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.eqType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.Exports [module, in mathcomp.algebra.ssrnum]
Num.NumField.Exports.numFieldType [abbreviation, in mathcomp.algebra.ssrnum]
[ numFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
Num.NumField.fieldType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.idomainType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.join_numDomainType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.mixin [projection, in mathcomp.algebra.ssrnum]
Num.NumField.numDomainType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.pack [definition, in mathcomp.algebra.ssrnum]
Num.NumField.Pack [constructor, in mathcomp.algebra.ssrnum]
Num.NumField.ringType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.sort [projection, in mathcomp.algebra.ssrnum]
Num.NumField.type [record, in mathcomp.algebra.ssrnum]
Num.NumField.unitRingType [definition, in mathcomp.algebra.ssrnum]
Num.NumField.xclass [abbreviation, in mathcomp.algebra.ssrnum]
Num.NumField.zmodType [definition, in mathcomp.algebra.ssrnum]
Num.num_for [abbreviation, in mathcomp.algebra.ssrnum]
Num.pos [abbreviation, in mathcomp.algebra.ssrnum]
Num.PredInstances [module, in mathcomp.algebra.ssrnum]
Num.real [abbreviation, in mathcomp.algebra.ssrnum]
Num.RealClosedField [module, in mathcomp.algebra.ssrnum]
Num.RealClosedField.base [projection, in mathcomp.algebra.ssrnum]
Num.RealClosedField.choiceType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.class [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.Class [constructor, in mathcomp.algebra.ssrnum]
Num.RealClosedField.ClassDef [section, in mathcomp.algebra.ssrnum]
Num.RealClosedField.ClassDef.cT [variable, in mathcomp.algebra.ssrnum]
Num.RealClosedField.ClassDef.T [variable, in mathcomp.algebra.ssrnum]
Num.RealClosedField.ClassDef.xT [variable, in mathcomp.algebra.ssrnum]
Num.RealClosedField.class_of [record, in mathcomp.algebra.ssrnum]
Num.RealClosedField.clone [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.comRingType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.comUnitRingType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.eqType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.Exports [module, in mathcomp.algebra.ssrnum]
Num.RealClosedField.Exports.RcfType [abbreviation, in mathcomp.algebra.ssrnum]
Num.RealClosedField.Exports.rcfType [abbreviation, in mathcomp.algebra.ssrnum]
[ rcfType of _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ rcfType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
Num.RealClosedField.fieldType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.idomainType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.numDomainType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.numFieldType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.pack [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.Pack [constructor, in mathcomp.algebra.ssrnum]
Num.RealClosedField.realDomainType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.realFieldType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.ringType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.sort [projection, in mathcomp.algebra.ssrnum]
Num.RealClosedField.type [record, in mathcomp.algebra.ssrnum]
Num.RealClosedField.unitRingType [definition, in mathcomp.algebra.ssrnum]
Num.RealClosedField.xclass [abbreviation, in mathcomp.algebra.ssrnum]
Num.RealClosedField.zmodType [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain [module, in mathcomp.algebra.ssrnum]
Num.RealDomain.base [projection, in mathcomp.algebra.ssrnum]
Num.RealDomain.choiceType [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.class [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.Class [constructor, in mathcomp.algebra.ssrnum]
Num.RealDomain.ClassDef [section, in mathcomp.algebra.ssrnum]
Num.RealDomain.ClassDef.cT [variable, in mathcomp.algebra.ssrnum]
Num.RealDomain.ClassDef.T [variable, in mathcomp.algebra.ssrnum]
Num.RealDomain.ClassDef.xT [variable, in mathcomp.algebra.ssrnum]
Num.RealDomain.class_of [record, in mathcomp.algebra.ssrnum]
Num.RealDomain.clone [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.comRingType [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.comUnitRingType [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.eqType [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.Exports [module, in mathcomp.algebra.ssrnum]
Num.RealDomain.Exports.RealDomainType [abbreviation, in mathcomp.algebra.ssrnum]
Num.RealDomain.Exports.realDomainType [abbreviation, in mathcomp.algebra.ssrnum]
[ realDomainType of _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ realDomainType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
Num.RealDomain.idomainType [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.numDomainType [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.pack [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.Pack [constructor, in mathcomp.algebra.ssrnum]
Num.RealDomain.ringType [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.sort [projection, in mathcomp.algebra.ssrnum]
Num.RealDomain.type [record, in mathcomp.algebra.ssrnum]
Num.RealDomain.unitRingType [definition, in mathcomp.algebra.ssrnum]
Num.RealDomain.xclass [abbreviation, in mathcomp.algebra.ssrnum]
Num.RealDomain.zmodType [definition, in mathcomp.algebra.ssrnum]
Num.RealField [module, in mathcomp.algebra.ssrnum]
Num.RealField.base [projection, in mathcomp.algebra.ssrnum]
Num.RealField.base2 [definition, in mathcomp.algebra.ssrnum]
Num.RealField.choiceType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.class [definition, in mathcomp.algebra.ssrnum]
Num.RealField.Class [constructor, in mathcomp.algebra.ssrnum]
Num.RealField.ClassDef [section, in mathcomp.algebra.ssrnum]
Num.RealField.ClassDef.cT [variable, in mathcomp.algebra.ssrnum]
Num.RealField.ClassDef.T [variable, in mathcomp.algebra.ssrnum]
Num.RealField.ClassDef.xT [variable, in mathcomp.algebra.ssrnum]
Num.RealField.class_of [record, in mathcomp.algebra.ssrnum]
Num.RealField.comRingType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.comUnitRingType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.eqType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.Exports [module, in mathcomp.algebra.ssrnum]
Num.RealField.Exports.realFieldType [abbreviation, in mathcomp.algebra.ssrnum]
[ realFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
Num.RealField.fieldType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.idomainType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.join_numFieldType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.join_fieldType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.mixin [projection, in mathcomp.algebra.ssrnum]
Num.RealField.numDomainType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.numFieldType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.pack [definition, in mathcomp.algebra.ssrnum]
Num.RealField.Pack [constructor, in mathcomp.algebra.ssrnum]
Num.RealField.realDomainType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.ringType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.sort [projection, in mathcomp.algebra.ssrnum]
Num.RealField.type [record, in mathcomp.algebra.ssrnum]
Num.RealField.unitRingType [definition, in mathcomp.algebra.ssrnum]
Num.RealField.xclass [abbreviation, in mathcomp.algebra.ssrnum]
Num.RealField.zmodType [definition, in mathcomp.algebra.ssrnum]
Num.RealMixin [module, in mathcomp.algebra.ssrnum]
Num.RealMixin.eq0_norm [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.Le [definition, in mathcomp.algebra.ssrnum]
Num.RealMixin.le_total [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.le_normD [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.le_def [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.le0_total [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.le0_anti [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.le0_mul [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.le0_add [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.Lt [definition, in mathcomp.algebra.ssrnum]
Num.RealMixin.lt_def [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.lt0_add [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.normM [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.Real [lemma, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins [section, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.le [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin [section, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.ge0_norm [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.leN_total [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.le0N [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.le0_total [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.le0_anti [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.le0_mul [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.le0_add [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.le00 [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.le01 [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.lt_def [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.normN [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LeMixin.sub_ge0 [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.lt [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LtMixin [section, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LtMixin.ge0_norm [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LtMixin.le_def [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LtMixin.lt0_total [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LtMixin.lt0_ngt0 [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LtMixin.lt0_mul [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LtMixin.lt0_add [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LtMixin.normN [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.LtMixin.sub_gt0 [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.norm [variable, in mathcomp.algebra.ssrnum]
Num.RealMixin.RealMixins.R [variable, in mathcomp.algebra.ssrnum]
`| _ | (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ < _ [notation, in mathcomp.algebra.ssrnum]
_ <= _ [notation, in mathcomp.algebra.ssrnum]
Num.RealMixin.sub_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.real_closed_axiom [definition, in mathcomp.algebra.ssrnum]
Num.real_axiom [definition, in mathcomp.algebra.ssrnum]
Num.ring_for [abbreviation, in mathcomp.algebra.ssrnum]
Num.sg [abbreviation, in mathcomp.algebra.ssrnum]
Num.sqrt [abbreviation, in mathcomp.algebra.ssrnum]
Num.Syntax [module, in mathcomp.algebra.ssrnum]
_ <= _ ?= iff _ :> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ <= _ ?= iff _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ < _ < _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ <= _ < _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ < _ <= _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ <= _ <= _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ >= _ :> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ >= _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ <= _ :> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ <= _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ > _ :> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ > _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ < _ :> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ < _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
>= _ :> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
>= _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
<= _ :> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
<= _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
> _ :> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
< _ :> _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
< _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
[notation, in mathcomp.algebra.ssrnum]
>=%R (ring_scope) [notation, in mathcomp.algebra.ssrnum]
<=%R (ring_scope) [notation, in mathcomp.algebra.ssrnum]
>%R (ring_scope) [notation, in mathcomp.algebra.ssrnum]
<%R (ring_scope) [notation, in mathcomp.algebra.ssrnum]
`| _ | (ring_scope) [notation, in mathcomp.algebra.ssrnum]
Num.Theory [module, in mathcomp.algebra.ssrnum]
Num.Theory.addC_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.addr_maxr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.addr_maxl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.addr_minr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.addr_minl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.addr_max_min [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.addr_min_max [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.addr_ss_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.addr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.addr_gt0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ArchimedeanFieldTheory [section, in mathcomp.algebra.ssrnum]
Num.Theory.ArchimedeanFieldTheory.F [variable, in mathcomp.algebra.ssrnum]
Num.Theory.ArchimedeanFieldTheory.x [variable, in mathcomp.algebra.ssrnum]
Num.Theory.archi_boundP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.argCle [definition, in mathcomp.algebra.ssrnum]
Num.Theory.arg_maxrP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.arg_minrP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.arg_maxr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.arg_minr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.Cauchy_root_bound [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.char_num [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ClosedFieldTheory [section, in mathcomp.algebra.ssrnum]
Num.Theory.ClosedFieldTheory.argCleP [variable, in mathcomp.algebra.ssrnum]
Num.Theory.ClosedFieldTheory.C [variable, in mathcomp.algebra.ssrnum]
Num.Theory.ClosedFieldTheory.neg_unity_root [variable, in mathcomp.algebra.ssrnum]
Num.Theory.ClosedFieldTheory.nz2 [variable, in mathcomp.algebra.ssrnum]
Num.Theory.ClosedFieldTheory.Re2 [variable, in mathcomp.algebra.ssrnum]
'Im _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
'Re _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ .-root (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ .-root (ring_scope) [notation, in mathcomp.algebra.ssrnum]
Num.Theory.comparer [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.ComparerEq [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ComparerEq0 [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ComparerGt [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ComparerGt0 [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ComparerLt [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ComparerLt0 [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.comparer0 [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.conjC [definition, in mathcomp.algebra.ssrnum]
Num.Theory.conjCi [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.conjCK [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.conjC_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.conjC_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.conjC_nat [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.conjC_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.conjC0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.conjC1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.conj_normC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.conj_Creal [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.cpr_add [definition, in mathcomp.algebra.ssrnum]
Num.Theory.CrealE [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.CrealP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Creal_ReP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Creal_ImP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Creal_Im [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Creal_Re [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Crect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.decnr_inj_inj_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.decnr_inj_inj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.decrn_inj_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.decrn_inj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.decr_inj_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.decr_inj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.distrC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.divr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.divr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqC_semipolar [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_sqrtC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_rootC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_sqrt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_maxr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_maxl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_minr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_minl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_norm2 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_norml [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_ltRL [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_ltLR [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_leRL [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_leLR [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_norm_idVN [definition, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_normN [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_norm_id [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_expn2 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_nat [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_muln2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_pmuln2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.eqr_le [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprCK [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_odd_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_odd_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_odd_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_odd_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_even_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_even_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_even_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_even_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_cp1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_egte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_egt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_ege1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_ilte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_ilt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_ile1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_gte0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.exprn_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.expr_gte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.expr_gt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.expr_ge1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.expr_lte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.expr_lt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.expr_le1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.FinGroup [section, in mathcomp.algebra.ssrnum]
Num.Theory.FinGroup.gT [variable, in mathcomp.algebra.ssrnum]
Num.Theory.FinGroup.R [variable, in mathcomp.algebra.ssrnum]
Num.Theory.geC0_unit_exp [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.geC0_conj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gerE [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.GerNotLt [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ger_lerif [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger_nmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger_nmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger_pmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger_pmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger_addr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger_addl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger_sub_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger_leVge [definition, in mathcomp.algebra.ssrnum]
Num.Theory.Ger0NotLt0 [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ger0P [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger0_xor_lt0 [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.ger0_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger0_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger0_def [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ger1_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ge0_cp [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gtrE [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.GtrNotLe [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.gtr_nmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gtr_nmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gtr_pmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gtr_pmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gtr_addr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gtr_addl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gtr_eqF [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Gtr0NotGt0 [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.gtr0_sg [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gtr0_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.gtr0_norm [definition, in mathcomp.algebra.ssrnum]
Num.Theory.gt0_cp [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ieexprIn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ieexprn_weq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Im [definition, in mathcomp.algebra.ssrnum]
Num.Theory.imaginaryC [definition, in mathcomp.algebra.ssrnum]
Num.Theory.imaginaryCE [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ImMl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ImMr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Im_rootC_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Im_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Im_conj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Im_i [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Im_is_additive [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.incnr_inj_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.incnr_inj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.incrn_inj_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.incrn_inj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.incr_inj_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.incr_inj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_nhomo_ltrn_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_homo_ltrn_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_nhomo_ltrn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_homo_ltrn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_nhomo_ltnr_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_homo_ltnr_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_nhomo_ltnr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_homo_ltnr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_nhomo_ltr_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_homo_ltr_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_nhomo_ltr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.inj_homo_ltr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invCi [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invC_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invC_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invf_cp1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.invf_lte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.invf_lt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invf_le1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invf_gte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.invf_ge1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invf_gt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invr_sg [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invr_cp1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.invr_lte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.invr_lt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invr_le1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invr_gte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.invr_ge1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invr_gt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invr_lte0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.invr_gte0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.invr_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invr_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.invr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.IsNoSqrtr [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.IsSqrtr [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.lef_ninv [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lef_pinv [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lenrW_nmono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lenrW_mono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lenrW_nmono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lenrW_mono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lenr_nmono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lenr_mono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lenr_nmono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lenr_mono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerifP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_rootC_AGM [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_Re_Creal [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_normC_Re_Creal [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_AGM2 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_mean_square [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_AGM2_scaled [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_mean_square_scaled [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_AGM [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_AGM_scaled [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_pprod [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_nmul [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_pmul [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_0_sum [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_sum [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_add [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_subRL [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_subLR [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_nat [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_eq [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_le [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_trans [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerif_refl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerNgt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.LerNotGt [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.lernW_nmono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lernW_mono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lernW_nmono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lernW_mono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lern_nmono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lern_mono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lern_nmono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lern_mono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lern0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lern1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerN10 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerW_nmono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerW_mono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerW_nmono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lerW_mono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sqrtC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_rootC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_rootCl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sqrt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_psqrt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_wsqrtr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_maxl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_maxr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_minl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_minr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_distl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_normr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_normlP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_norml [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nmono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_mono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nmono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_mono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_total [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivr_mull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivl_mull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivr_mulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivl_mulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pdivr_mull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pdivl_mull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pdivr_mulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pdivl_mulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nnorml [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_dist_norm_add [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_dist_dist [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sub_dist [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sub_norm_add [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_dist_add [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_norm_sub [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_norm_sum [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_ninv [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pinv [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sqr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pexpn2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_expn2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_eexpn2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_iexpn2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_weexpn2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_wiexpn2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_eexpr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_iexpr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nimulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pimulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nimull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pimull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nemulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pemulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nemull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pemull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_prod [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nat [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nmuln2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pmuln2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_wnmuln2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_wpmuln2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_muln2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_wmuln2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pmuln2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pmul [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_wnmul2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_wnmul2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_wpmul2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_wpmul2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nmul2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_nmul2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pmul2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_pmul2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sum [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_naddr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_paddr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_naddl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_paddl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_addr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_addl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sub_addl [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ler_subr_addl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_subl_addl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sub_addr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ler_subr_addr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_subl_addr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_lt_sub [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sub [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_lt_add [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_add [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_add2 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ler_add2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_add2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_sub_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_xor_gt [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.ler_leVge [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_oppl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_oppr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_opp2 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_gtF [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_lt_asym [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_anti [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_trans [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_lt_trans [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_asym [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_eqVlt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler_def [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ler_norm_add [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ler0n [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Ler0NotLe0 [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ler0N1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler0P [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler0_sqrtr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler0_xor_gt0 [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.ler0_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler0_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler0_def [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler01 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler1n [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler1_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ler10 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.le0r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.le0_cp [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltef_ninv [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ltef_pinv [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lterr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_maxl [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_maxr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_minl [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_minr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_distl [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_normr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_norml [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_ndivr_mull [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_ndivl_mull [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_ndivr_mulr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_ndivl_mulr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_pdivr_mull [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_pdivl_mull [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_pdivr_mulr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_pdivl_mulr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_nnormr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_pexpn2r [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_expn2r [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_eexpn2l [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_iexpn2l [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_expr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_eexpr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_iexpr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_nmul2r [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_nmul2l [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_pmul2r [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_pmul2l [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_sub_addl [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_sub_addr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_add2 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_oppE [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_oppl [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_oppr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_opp2 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter_anti [definition, in mathcomp.algebra.ssrnum]
Num.Theory.lter01 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ltf_ninv [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltf_pinv [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltnrW_nhomo_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltnrW_homo_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltnrW_nhomo [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltnrW_homo [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrgtP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrgt0P [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrNge [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.LtrNotGe [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ltrnW_nhomo_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrnW_homo_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrnW_nhomo [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrnW_homo [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrn0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrn1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrN10 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrW [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrW_nhomo_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrW_homo_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrW_nhomo [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltrW_homo [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_sqrtC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_rootC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_rootCl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_sqrt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_maxl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_maxr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_minl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_minr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_distl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_normr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_normlP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_norml [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_total [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_ndivr_mull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_ndivl_mull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_ndivr_mulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_ndivl_mulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pdivr_mull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pdivl_mull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pdivr_mulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pdivl_mulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_lerif [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nnorml [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_ninv [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pinv [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_sqr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pexpn2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wpexpn2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_expn2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_eexpn2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_iexpn2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_eexpr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_iexpr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_prod_nat [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_prod [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nat [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nmuln2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pmuln2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_muln2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wpmuln2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wmuln2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pmuln2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pmul [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nmul2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nmul2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pmul2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pmul2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_snsaddr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_snaddr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_naddr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_spsaddr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_spaddr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_paddr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_snsaddl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_snaddl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_naddl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_spsaddl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_spaddl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_paddl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_addr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_addl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_sub_addl [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_subr_addl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_subl_addl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_sub_addr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_subr_addr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_subl_addr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_sub [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_le_sub [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_add [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_le_add [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_add2 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_add2r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_add2l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_xor_ge [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_oppl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_oppr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_opp2 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_gtF [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_geF [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_le_asym [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_asym [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_le_trans [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_trans [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_eqF [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_neqAle [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr_def [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ltr0n [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Ltr0NotGe0 [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.ltr0N1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr0Sn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_sqrtr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_sg [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_norm [definition, in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_neq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr01 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr1n [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ltr10 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lt0r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lt0r_neq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.lt0_cp [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxNr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxrA [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxrAC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxrC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxrCA [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxrN [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxrP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxrr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_nmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_pmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_nmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_pmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_minr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_minl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Maxr_l [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.Maxr_r [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_spec [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_to_min [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.maxr_l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mid [abbreviation, in mathcomp.algebra.ssrnum]
Num.Theory.midf_lte [definition, in mathcomp.algebra.ssrnum]
Num.Theory.midf_lt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.midf_le [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minKr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minNr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minrA [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minrAC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minrC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minrCA [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minrK [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minrN [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minrP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minrr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minr_nmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minr_pmull [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minr_nmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minr_pmulr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minr_maxr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minr_maxl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Minr_l [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.Minr_r [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.minr_spec [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.minr_to_max [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minr_r [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.minr_l [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.monic_Cauchy_bound [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mono_lerif [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mono_in_lerif [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulC_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulrIn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_wlt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_wgt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_wle0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_wge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sg_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_Nsign_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sign_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sign_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sg_eqN1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sg_eq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_cp1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_egte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_egt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ege1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ilte1 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ilt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ile1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_le0_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ge0_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mul_conjC_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mul_conjC_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.mul_conjC_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.naddr_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.natf_indexg [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.natf_div [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.natrG_neq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.natrG_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.natr_indexg_neq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.natr_indexg_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.negrE [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.neqr_lt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.neqr0_sign [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.neq0Ci [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.neq0_mulr_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmono_lerif [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmono_in_lerif [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulrn_rle0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulrn_rge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulrn_rgt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_lle0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_llt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_lge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_lgt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_rle0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_rlt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_rge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_rgt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nnegIm [definition, in mathcomp.algebra.ssrnum]
Num.Theory.nnegrE [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nonRealCi [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normCi [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normCK [definition, in mathcomp.algebra.ssrnum]
Num.Theory.normCKC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC_sub_eq [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC_sum_upper [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC_sum_eq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC_sum_eq [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC_add_eq [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC_Re_Im [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC_def [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC2_Re_Im [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normC2_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normfV [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normf_div [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normrE [definition, in mathcomp.algebra.ssrnum]
Num.Theory.normrEsg [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normrEsign [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normrM [definition, in mathcomp.algebra.ssrnum]
Num.Theory.normrMn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normrMsign [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normrN [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normrN1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normrV [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normrX [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_sg [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_sign [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_id [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_eq0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.normr_unit [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_prod [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_nat [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr_idP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr0P [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.normr0_eq0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.normr1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.norm_conjC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.norm_rootC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Nreal_gtF [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Nreal_ltF [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Nreal_geF [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Nreal_leF [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.nthroot [definition, in mathcomp.algebra.ssrnum]
Num.Theory.NumDomainMonotonyTheoryForReals [section, in mathcomp.algebra.ssrnum]
Num.Theory.NumDomainMonotonyTheoryForReals.D [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumDomainMonotonyTheoryForReals.f [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumDomainMonotonyTheoryForReals.f' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumDomainMonotonyTheoryForReals.R [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumDomainMonotonyTheoryForReals.R' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumDomainOperationTheory [section, in mathcomp.algebra.ssrnum]
Num.Theory.NumDomainOperationTheory.R [variable, in mathcomp.algebra.ssrnum]
Num.Theory.numEsg [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.numEsign [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.NumFieldTheory [section, in mathcomp.algebra.ssrnum]
Num.Theory.NumFieldTheory.F [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory [section, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes [section, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes.D [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes.D' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.AcrossTypes.f [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.geq_total [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.geq_anti [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.ger_antiR' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.ger_antiR [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.gtnE [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.gtrE [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.gtr'E [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.leqnn [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.leq_total [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.leq_anti [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.ler_antiR' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.ler_antiR [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.ltnE [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.ltrE [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.ltr'E [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.NatToR [section, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.NatToR.D [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.NatToR.D' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.NatToR.f [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.R [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.RToNat [section, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.RToNat.D [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.RToNat.D' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.RToNat.f [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainMonotonyTheory.R' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainTheory [section, in mathcomp.algebra.ssrnum]
Num.Theory.NumIntegralDomainTheory.R [variable, in mathcomp.algebra.ssrnum]
Num.Theory.numNEsign [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.num_real [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.oppC_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.oppr_min [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.oppr_max [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.oppr_cp0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.oppr_lte0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.oppr_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.oppr_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.oppr_gte0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.oppr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.oppr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.paddr_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pexpIrn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pexprn_eq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pexpr_eq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulrnI [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_rle0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_rge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_rlt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_rgt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_lle0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_lge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_llt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_lgt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_lle0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_llt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_lge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_lgt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_rle0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_rlt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_rge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_rgt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pnatr_eq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.pnatr_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.poly_ivt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.poly_itv_bound [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.poly_disk_bound [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.posrE [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.prodr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.prodr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.psumr_eq0P [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.psumr_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Re [definition, in mathcomp.algebra.ssrnum]
Num.Theory.realB [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realBC [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.RealClosedFieldTheory [section, in mathcomp.algebra.ssrnum]
Num.Theory.RealClosedFieldTheory.R [variable, in mathcomp.algebra.ssrnum]
Num.Theory.realD [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainArgExtremum [section, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainMonotony [section, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainMonotony.D [variable, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainMonotony.f [variable, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainMonotony.f' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainMonotony.R [variable, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainMonotony.R' [variable, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainOperations [section, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainOperations.MinMax [section, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainOperations.PolyBounds [section, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainOperations.PolyBounds.p [variable, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainOperations.R [variable, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainTheory [section, in mathcomp.algebra.ssrnum]
Num.Theory.RealDomainTheory.R [variable, in mathcomp.algebra.ssrnum]
Num.Theory.realE [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realEsg [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realEsign [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realEsqr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.RealField [section, in mathcomp.algebra.ssrnum]
Num.Theory.RealField.F [variable, in mathcomp.algebra.ssrnum]
Num.Theory.RealField.x [variable, in mathcomp.algebra.ssrnum]
Num.Theory.RealField.y [variable, in mathcomp.algebra.ssrnum]
Num.Theory.realM [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realMr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realN [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realNEsign [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realn_nmono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realn_mono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realn_nmono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realn_mono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realrM [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realrMn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realV [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.realX [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lerif_AGM2 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lerif_mean_square [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_nmono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_mono_in [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_nmono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_mono [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lerif_AGM2_scaled [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lerif_mean_square_scaled [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lerif_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_mulr_Nsign_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_mulr_sign_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_normrEsign [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_normK [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_odd_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_odd_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_odd_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_odd_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_even_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_even_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_even_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_even_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lter_distl [definition, in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_distl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_distl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lter_normr [definition, in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_normr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_normr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_normlP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lter_norml [definition, in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_norml [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_eqr_norm2 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_eqr_norml [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_normlP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_norml [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_wlog_ltr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_wlog_ler [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_neqr_lt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ltrgt0P [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ler0P [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ger0P [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ltrgtP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lerNgt [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ltrNge [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_ltrP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_lerP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real_leVge [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.real1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ReMl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.ReMr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Re_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Re_conj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Re_i [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.Re_is_additive [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootCK [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootCMl [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootCMr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootCpX [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.RootCspec [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.rootCV [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootCX [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_lt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_le1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_gt1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_ge1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_eq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_Re_max [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_inj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_subproof [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC_spec [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.rootC0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.rootC1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.root0C [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.root1C [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgrE [definition, in mathcomp.algebra.ssrnum]
Num.Theory.sgrM [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgrMn [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgrN [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.SgrNeg [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.SgrNull [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.sgrN1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgrP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.SgrPos [constructor, in mathcomp.algebra.ssrnum]
Num.Theory.sgrV [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgrX [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_smul [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_val [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_cp0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_norm [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_id [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_nat [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_odd [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr_def [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sgr1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.signr_inj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.signr_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.signr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.signr_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.signr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrCi [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrCK [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrCK_P [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrn_eq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrp_eq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC [abbreviation, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC [abbreviation, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtCK [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtCM [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_inj [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtrM [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtrP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr_eq0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr_sqr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr_spec [inductive, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqr_sqrtr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqr_norm_eq1 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sqr_sg [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.subC_rect [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.subr_cp0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.subr_gte0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.subr_lte0 [definition, in mathcomp.algebra.ssrnum]
Num.Theory.subr_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.subr_le0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.subr_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.subr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.sumr_ge0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.unitf_lt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.unitf_gt0 [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.upper_nthrootP [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.wlog_ltr [lemma, in mathcomp.algebra.ssrnum]
Num.Theory.wlog_ler [lemma, in mathcomp.algebra.ssrnum]
[ arg maxr_ ( _ > _ ) _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ arg maxr_ ( _ > _ in _ ) _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ arg maxr_ ( _ > _ | _ ) _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ arg minr_ ( _ < _ ) _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ arg minr_ ( _ < _ in _ ) _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
[ arg minr_ ( _ < _ | _ ) _ ] (form_scope) [notation, in mathcomp.algebra.ssrnum]
'Im _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
'Re _ (ring_scope) [notation, in mathcomp.algebra.ssrnum]
'i (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ .-root (ring_scope) [notation, in mathcomp.algebra.ssrnum]
'i (ring_scope) [notation, in mathcomp.algebra.ssrnum]
_ ^* (ring_scope) [notation, in mathcomp.algebra.ssrnum]
nz_socle [lemma, in mathcomp.character.mxrepresentation]
nz_row_mxsimple [lemma, in mathcomp.character.mxrepresentation]
nz_row_eq0 [lemma, in mathcomp.algebra.matrix]
nz_row [definition, in mathcomp.algebra.matrix]
nz_row_sub [lemma, in mathcomp.algebra.mxalgebra]
n_act_add [lemma, in mathcomp.solvable.primitive_action]
n_act0 [lemma, in mathcomp.solvable.primitive_action]
n_act_dtuple [lemma, in mathcomp.solvable.primitive_action]
n_act_is_action [lemma, in mathcomp.solvable.primitive_action]
n_act [definition, in mathcomp.solvable.primitive_action]
n_comp_connect [lemma, in mathcomp.ssreflect.fingraph]
n_comp_closure2 [lemma, in mathcomp.ssreflect.fingraph]
n_compC [lemma, in mathcomp.ssreflect.fingraph]
n_comp [abbreviation, in mathcomp.ssreflect.fingraph]
n_comp_mem [definition, in mathcomp.ssreflect.fingraph]
n' [abbreviation, in mathcomp.character.mxabelem]
| 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 | _ | other | (24263 entries) |
| Notation 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 | _ | other | (1399 entries) |
| Module 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 | _ | other | (226 entries) |
| Variable 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 | _ | other | (3670 entries) |
| Library 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 | _ | other | (89 entries) |
| Lemma 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 | _ | other | (12297 entries) |
| Constructor 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 | _ | other | (383 entries) |
| Axiom 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 | _ | other | (45 entries) |
| Inductive 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 | _ | other | (114 entries) |
| Projection 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 | _ | other | (279 entries) |
| Section 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 | _ | other | (1169 entries) |
| Abbreviation 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 | _ | other | (742 entries) |
| Definition 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 | _ | other | (3657 entries) |
| Record 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 | _ | other | (193 entries) |