| 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 | (54001 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 | (1931 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 | (1658 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 | (7199 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 | (97 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 | (15214 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 | (75 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 | (224 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 | (132 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 | (2371 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 | (2266 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 | (732 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 | (21455 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 | (647 entries) |
N (lemma)
nary_addv_subproof [in mathcomp.algebra.vector]nary_mxsum_proof [in mathcomp.algebra.mxalgebra]
natn [in mathcomp.algebra.ssralg]
natnseq0P [in mathcomp.ssreflect.seq]
natq_div [in mathcomp.algebra.rat]
natrDE [in mathcomp.algebra.ssralg]
natrME [in mathcomp.algebra.ssralg]
natrXE [in mathcomp.algebra.ssralg]
natr_negZp [in mathcomp.algebra.zmodp]
natr_Zp [in mathcomp.algebra.zmodp]
natr_absz [in mathcomp.algebra.ssrint]
natr0E [in mathcomp.algebra.ssralg]
natr1E [in mathcomp.algebra.ssralg]
natsum_of_intK [in mathcomp.algebra.ssrint]
NatTrec.addE [in mathcomp.ssreflect.ssrnat]
NatTrec.add_mulE [in mathcomp.ssreflect.ssrnat]
NatTrec.doubleE [in mathcomp.ssreflect.ssrnat]
NatTrec.expE [in mathcomp.ssreflect.ssrnat]
NatTrec.mulE [in mathcomp.ssreflect.ssrnat]
NatTrec.mul_expE [in mathcomp.ssreflect.ssrnat]
NatTrec.oddE [in mathcomp.ssreflect.ssrnat]
natz [in mathcomp.algebra.ssrint]
nat_pickleK [in mathcomp.ssreflect.choice]
nat_hasChoice [in mathcomp.ssreflect.choice]
nat_power_theory [in mathcomp.ssreflect.ssrnat]
nat_semi_morph [in mathcomp.ssreflect.ssrnat]
nat_semi_ring [in mathcomp.ssreflect.ssrnat]
nat_of_exp_bin [in mathcomp.ssreflect.ssrnat]
nat_of_mul_bin [in mathcomp.ssreflect.ssrnat]
nat_of_add_bin [in mathcomp.ssreflect.ssrnat]
nat_of_mul_pos [in mathcomp.ssreflect.ssrnat]
nat_of_add_pos [in mathcomp.ssreflect.ssrnat]
nat_of_succ_pos [in mathcomp.ssreflect.ssrnat]
nat_of_binK [in mathcomp.ssreflect.ssrnat]
nat_AGM2 [in mathcomp.ssreflect.ssrnat]
nat_Cauchy [in mathcomp.ssreflect.ssrnat]
nat_irrelevance [in mathcomp.ssreflect.ssrnat]
nclasses_isog [in mathcomp.fingroup.morphism]
nclasses_injm [in mathcomp.fingroup.morphism]
nconsK [in mathcomp.ssreflect.seq]
ncprodS [in mathcomp.solvable.center]
ncprod_key [in mathcomp.solvable.center]
ncprod0 [in mathcomp.solvable.center]
ncprod1 [in mathcomp.solvable.center]
nderivnB [in mathcomp.algebra.poly]
nderivnC [in mathcomp.algebra.poly]
nderivnD [in mathcomp.algebra.poly]
nderivnMn [in mathcomp.algebra.poly]
nderivnMNn [in mathcomp.algebra.poly]
nderivnMXaddC [in mathcomp.algebra.poly]
nderivnN [in mathcomp.algebra.poly]
nderivnXn [in mathcomp.algebra.poly]
nderivnZ [in mathcomp.algebra.poly]
nderivn_map [in mathcomp.algebra.poly]
nderivn_poly0 [in mathcomp.algebra.poly]
nderivn_is_linear [in mathcomp.algebra.poly]
nderivn_def [in mathcomp.algebra.poly]
nderivn0 [in mathcomp.algebra.poly]
nderivn1 [in mathcomp.algebra.poly]
nderiv_taylor_wide [in mathcomp.algebra.poly]
nderiv_taylor [in mathcomp.algebra.poly]
ndirrK [in mathcomp.character.vcharacter]
ndirr_inj [in mathcomp.character.vcharacter]
ndirr_diff [in mathcomp.character.vcharacter]
ndir_s0p [in mathcomp.solvable.burnside_app]
negb_exists_in [in mathcomp.ssreflect.fintype]
negb_exists [in mathcomp.ssreflect.fintype]
negb_forall_in [in mathcomp.ssreflect.fintype]
negb_forall [in mathcomp.ssreflect.fintype]
negb_eqb [in mathcomp.ssreflect.eqtype]
negb_add [in mathcomp.ssreflect.eqtype]
negb_row_free [in mathcomp.algebra.mxalgebra]
negnK [in mathcomp.ssreflect.prime]
NegzE [in mathcomp.algebra.ssrint]
nElemI [in mathcomp.solvable.abelian]
nElemP [in mathcomp.solvable.abelian]
nElemS [in mathcomp.solvable.abelian]
nElem0 [in mathcomp.solvable.abelian]
nElem1P [in mathcomp.solvable.abelian]
neq_ltn [in mathcomp.ssreflect.ssrnat]
neq_dim_orthov1 [in mathcomp.algebra.sesquilinear]
neq_lift [in mathcomp.ssreflect.fintype]
neq_bump [in mathcomp.ssreflect.fintype]
neq0CG [in mathcomp.character.classfun]
neq0CiG [in mathcomp.character.classfun]
neq0_lt0n [in mathcomp.ssreflect.ssrnat]
neq0_has_constt [in mathcomp.character.character]
nexpIrz [in mathcomp.algebra.ssrint]
nextE [in mathcomp.ssreflect.path]
next_map [in mathcomp.ssreflect.path]
next_rev [in mathcomp.ssreflect.path]
next_rotr [in mathcomp.ssreflect.path]
next_rot [in mathcomp.ssreflect.path]
next_prev [in mathcomp.ssreflect.path]
next_cycle [in mathcomp.ssreflect.path]
next_nth [in mathcomp.ssreflect.path]
nilP [in mathcomp.ssreflect.seq]
nilpE [in mathcomp.ssreflect.seq]
nilpotentS [in mathcomp.solvable.nilpotent]
nilpotent_pcoreC [in mathcomp.solvable.sylow]
nilpotent_pcore_Hall [in mathcomp.solvable.sylow]
nilpotent_Hall_pcore [in mathcomp.solvable.sylow]
nilpotent_maxp_normal [in mathcomp.solvable.sylow]
nilpotent_Fitting [in mathcomp.solvable.maximal]
nilpotent_sol [in mathcomp.solvable.nilpotent]
nilpotent_subnormal [in mathcomp.solvable.nilpotent]
nilpotent_proper_norm [in mathcomp.solvable.nilpotent]
nilpotent_sub_norm [in mathcomp.solvable.nilpotent]
nilpotent_class [in mathcomp.solvable.nilpotent]
nilpotent1 [in mathcomp.solvable.nilpotent]
nil_Zgroup_cyclic [in mathcomp.solvable.sylow]
nil_class_pgroup [in mathcomp.solvable.sylow]
nil_class3 [in mathcomp.solvable.sylow]
nil_class2 [in mathcomp.solvable.sylow]
nil_basis [in mathcomp.algebra.vector]
nil_free [in mathcomp.algebra.vector]
nil_poly [in mathcomp.algebra.poly]
nil_class_quotient_center [in mathcomp.solvable.nilpotent]
nil_class_injm [in mathcomp.solvable.nilpotent]
nil_class_morphim [in mathcomp.solvable.nilpotent]
nil_class_ucn [in mathcomp.solvable.nilpotent]
nil_class1 [in mathcomp.solvable.nilpotent]
nil_class0 [in mathcomp.solvable.nilpotent]
nil_comm_properr [in mathcomp.solvable.nilpotent]
nil_comm_properl [in mathcomp.solvable.nilpotent]
NirrE [in mathcomp.character.character]
nmulrn [in mathcomp.algebra.ssrint]
nmulrz_rle0 [in mathcomp.algebra.ssrint]
nmulrz_rge0 [in mathcomp.algebra.ssrint]
nmulrz_rlt0 [in mathcomp.algebra.ssrint]
nmulrz_rgt0 [in mathcomp.algebra.ssrint]
nmulrz_lle0 [in mathcomp.algebra.ssrint]
nmulrz_lge0 [in mathcomp.algebra.ssrint]
nmulrz_llt0 [in mathcomp.algebra.ssrint]
nmulrz_lgt0 [in mathcomp.algebra.ssrint]
nonconform_mx [in mathcomp.algebra.matrix]
nonlinear_irr_vanish [in mathcomp.character.integral_char]
nontrivial_gacent_pgroup [in mathcomp.solvable.sylow]
nonzero1fx [in mathcomp.field.fieldext]
nonzero1q [in mathcomp.algebra.rat]
normalC [in mathcomp.algebra.sesquilinear]
normalD1 [in mathcomp.fingroup.fingroup]
normalE [in mathcomp.algebra.sesquilinear]
normalFieldf [in mathcomp.field.galois]
normalFieldP [in mathcomp.field.galois]
normalFieldS [in mathcomp.field.galois]
normalField_isog [in mathcomp.field.galois]
normalField_isom [in mathcomp.field.galois]
normalField_img [in mathcomp.field.galois]
normalField_normal [in mathcomp.field.galois]
normalField_ker [in mathcomp.field.galois]
normalField_castM [in mathcomp.field.galois]
normalField_cast_eq [in mathcomp.field.galois]
normalField_galois [in mathcomp.field.galois]
normalField_factors [in mathcomp.field.galois]
normalField_root_minPoly [in mathcomp.field.galois]
normalField_kAut [in mathcomp.field.galois]
normalG [in mathcomp.fingroup.fingroup]
normalGI [in mathcomp.fingroup.fingroup]
normalI [in mathcomp.fingroup.fingroup]
normalJ [in mathcomp.fingroup.fingroup]
normalM [in mathcomp.fingroup.fingroup]
normalmxP [in mathcomp.algebra.spectral]
normalmx_key [in mathcomp.algebra.spectral]
normalP [in mathcomp.fingroup.fingroup]
normalP [in mathcomp.algebra.sesquilinear]
normalS [in mathcomp.fingroup.fingroup]
normalSG [in mathcomp.fingroup.fingroup]
normalY [in mathcomp.fingroup.fingroup]
normalYl [in mathcomp.fingroup.fingroup]
normalYr [in mathcomp.fingroup.fingroup]
normal_cosetpre [in mathcomp.fingroup.quotient]
normal_fixedField_galois [in mathcomp.field.galois]
normal_field_splitting [in mathcomp.field.galois]
normal_Inertia [in mathcomp.character.inertia]
normal_inertia [in mathcomp.character.inertia]
normal_subnorm [in mathcomp.fingroup.fingroup]
normal_refl [in mathcomp.fingroup.fingroup]
normal_norm [in mathcomp.fingroup.fingroup]
normal_sub [in mathcomp.fingroup.fingroup]
normal_pgroup [in mathcomp.solvable.sylow]
normal_sylowP [in mathcomp.solvable.sylow]
normal_Hall_pcore [in mathcomp.solvable.pgroup]
normal_max_pgroup_Hall [in mathcomp.solvable.pgroup]
normal_sub_max_pgroup [in mathcomp.solvable.pgroup]
normal_rfix_mx_module [in mathcomp.character.mxrepresentation]
normal_rank1_structure [in mathcomp.solvable.extremal]
normal_subnormal [in mathcomp.solvable.gseries]
normal_mx_ortho [in mathcomp.algebra.sesquilinear]
normal_ortho_mx [in mathcomp.algebra.sesquilinear]
normal1 [in mathcomp.fingroup.fingroup]
normC [in mathcomp.fingroup.fingroup]
normCs [in mathcomp.fingroup.fingroup]
normC_lin_char [in mathcomp.character.character]
normD1 [in mathcomp.fingroup.fingroup]
normedTI_J [in mathcomp.solvable.frobenius]
normedTI_S [in mathcomp.solvable.frobenius]
normedTI_memJ_P [in mathcomp.solvable.frobenius]
normedTI_P [in mathcomp.solvable.frobenius]
normG [in mathcomp.fingroup.fingroup]
normJ [in mathcomp.fingroup.fingroup]
normP [in mathcomp.fingroup.fingroup]
normqE [in mathcomp.algebra.rat]
normrMz [in mathcomp.algebra.ssrint]
normr_sg [in mathcomp.algebra.ssrint]
normr_sgz [in mathcomp.algebra.ssrint]
normr_num_div [in mathcomp.algebra.rat]
normr_denq [in mathcomp.algebra.rat]
normsD [in mathcomp.fingroup.fingroup]
normsD1 [in mathcomp.fingroup.fingroup]
normsG [in mathcomp.fingroup.fingroup]
normsGI [in mathcomp.fingroup.fingroup]
normsI [in mathcomp.fingroup.fingroup]
normsIG [in mathcomp.fingroup.fingroup]
normsIs [in mathcomp.fingroup.fingroup]
normsM [in mathcomp.fingroup.fingroup]
normsP [in mathcomp.fingroup.fingroup]
normsR [in mathcomp.fingroup.fingroup]
normsRl [in mathcomp.solvable.commutator]
normsRr [in mathcomp.solvable.commutator]
normsU [in mathcomp.fingroup.fingroup]
normsY [in mathcomp.fingroup.fingroup]
norms_cent [in mathcomp.fingroup.fingroup]
norms_bigcup [in mathcomp.fingroup.fingroup]
norms_bigcap [in mathcomp.fingroup.fingroup]
norms_class_support [in mathcomp.fingroup.fingroup]
norms_norm [in mathcomp.fingroup.fingroup]
norms_gen [in mathcomp.fingroup.fingroup]
norms_cycle [in mathcomp.fingroup.fingroup]
norms1 [in mathcomp.fingroup.fingroup]
normT [in mathcomp.fingroup.fingroup]
norm_quotient_pre [in mathcomp.fingroup.quotient]
norm_conj_autE [in mathcomp.fingroup.automorphism]
norm_conj_isom [in mathcomp.fingroup.automorphism]
norm_conjg_im [in mathcomp.fingroup.automorphism]
norm_Inertia [in mathcomp.character.inertia]
norm_inertia [in mathcomp.character.inertia]
norm_normalI [in mathcomp.fingroup.fingroup]
norm_gen [in mathcomp.fingroup.fingroup]
norm_conj_norm [in mathcomp.fingroup.fingroup]
norm_rlcoset [in mathcomp.fingroup.fingroup]
norm_joinEr [in mathcomp.fingroup.fingroup]
norm_joinEl [in mathcomp.fingroup.fingroup]
norm_sub_max_pgroup [in mathcomp.solvable.pgroup]
norm_sub_rstabs_rfix_mx [in mathcomp.character.mxrepresentation]
norm_ratN [in mathcomp.algebra.rat]
norm_conj_cent [in mathcomp.solvable.hall]
norm1 [in mathcomp.fingroup.fingroup]
notin_iter [in mathcomp.ssreflect.finset]
not_simple_Alt_4 [in mathcomp.solvable.alt]
not_isog_Dn_DnQ [in mathcomp.solvable.extraspecial]
not_asubv0 [in mathcomp.field.falgebra]
npolyP [in mathcomp.algebra.qpoly]
npolypK [in mathcomp.algebra.qpoly]
npolyp_key [in mathcomp.algebra.qpoly]
npolyXE [in mathcomp.algebra.qpoly]
npolyX_gen [in mathcomp.algebra.qpoly]
npolyX_coords [in mathcomp.algebra.qpoly]
npolyX_full [in mathcomp.algebra.qpoly]
npolyX_free [in mathcomp.algebra.qpoly]
npoly_enum_uniq [in mathcomp.algebra.qpoly]
npoly_vect_axiom [in mathcomp.algebra.qpoly]
npoly_rV_K [in mathcomp.algebra.qpoly]
npoly_is_a_poly_of_size [in mathcomp.algebra.qpoly]
npoly_submod_closed [in mathcomp.algebra.qpoly]
nseqD [in mathcomp.ssreflect.seq]
nseqP [in mathcomp.ssreflect.seq]
nseq_tupleP [in mathcomp.ssreflect.tuple]
nthK [in mathcomp.ssreflect.seq]
nthP [in mathcomp.ssreflect.seq]
nth_mktuple [in mathcomp.ssreflect.tuple]
nth_flatten [in mathcomp.ssreflect.seq]
nth_shape [in mathcomp.ssreflect.seq]
nth_reshape [in mathcomp.ssreflect.seq]
nth_zip_cond [in mathcomp.ssreflect.seq]
nth_zip [in mathcomp.ssreflect.seq]
nth_scanl [in mathcomp.ssreflect.seq]
nth_cons_scanl [in mathcomp.ssreflect.seq]
nth_pairmap [in mathcomp.ssreflect.seq]
nth_mkseq [in mathcomp.ssreflect.seq]
nth_iota [in mathcomp.ssreflect.seq]
nth_index_map [in mathcomp.ssreflect.seq]
nth_map [in mathcomp.ssreflect.seq]
nth_incr_nth [in mathcomp.ssreflect.seq]
nth_rcons_cat_find [in mathcomp.ssreflect.seq]
nth_uniq [in mathcomp.ssreflect.seq]
nth_index [in mathcomp.ssreflect.seq]
nth_rev [in mathcomp.ssreflect.seq]
nth_take [in mathcomp.ssreflect.seq]
nth_drop [in mathcomp.ssreflect.seq]
nth_find [in mathcomp.ssreflect.seq]
nth_set_nth [in mathcomp.ssreflect.seq]
nth_nseq [in mathcomp.ssreflect.seq]
nth_ncons [in mathcomp.ssreflect.seq]
nth_rcons_default [in mathcomp.ssreflect.seq]
nth_rcons [in mathcomp.ssreflect.seq]
nth_cat [in mathcomp.ssreflect.seq]
nth_behead [in mathcomp.ssreflect.seq]
nth_last [in mathcomp.ssreflect.seq]
nth_seq1 [in mathcomp.ssreflect.seq]
nth_nil [in mathcomp.ssreflect.seq]
nth_default [in mathcomp.ssreflect.seq]
nth_fgraph_ord [in mathcomp.ssreflect.finfun]
nth_traject [in mathcomp.ssreflect.path]
nth_enum_rank [in mathcomp.ssreflect.fintype]
nth_enum_rank_in [in mathcomp.ssreflect.fintype]
nth_codom [in mathcomp.ssreflect.fintype]
nth_image [in mathcomp.ssreflect.fintype]
nth_ord_enum [in mathcomp.ssreflect.fintype]
nth_enum_ord [in mathcomp.ssreflect.fintype]
nth_lagrange [in mathcomp.algebra.qpoly]
nth_npolyX [in mathcomp.algebra.qpoly]
nth0 [in mathcomp.ssreflect.seq]
ntransitive_primitive [in mathcomp.solvable.primitive_action]
ntransitive_weak [in mathcomp.solvable.primitive_action]
ntransitive0 [in mathcomp.solvable.primitive_action]
ntransitive1 [in mathcomp.solvable.primitive_action]
nt_pnElem [in mathcomp.solvable.abelian]
nt_prime_order [in mathcomp.solvable.cyclic]
nt_gen_prime [in mathcomp.solvable.cyclic]
numer_Ratio [in mathcomp.algebra.fraction]
numqE [in mathcomp.algebra.rat]
numqK [in mathcomp.algebra.rat]
numqN [in mathcomp.algebra.rat]
numq_lt0 [in mathcomp.algebra.rat]
numq_gt0 [in mathcomp.algebra.rat]
numq_le0 [in mathcomp.algebra.rat]
numq_ge0 [in mathcomp.algebra.rat]
numq_div_lt0 [in mathcomp.algebra.rat]
numq_sign_mul [in mathcomp.algebra.rat]
numq_int [in mathcomp.algebra.rat]
numq_eq0 [in mathcomp.algebra.rat]
num_field_proj [in mathcomp.field.algnum]
num_field_exists [in mathcomp.field.algnum]
num_fracq [in mathcomp.algebra.rat]
Num.Builders_19.truncP [in mathcomp.algebra.archimedean]
Num.Builders_19.trunc_subproof [in mathcomp.algebra.archimedean]
Num.Builders_19.boundP [in mathcomp.algebra.archimedean]
Num.Builders_70.le_total [in mathcomp.algebra.ssrnum]
Num.Builders_70.lt_def [in mathcomp.algebra.ssrnum]
Num.Builders_70.le_def' [in mathcomp.algebra.ssrnum]
Num.Builders_70.eq0_norm [in mathcomp.algebra.ssrnum]
Num.Builders_70.le_normD [in mathcomp.algebra.ssrnum]
Num.Builders_70.normM [in mathcomp.algebra.ssrnum]
Num.Builders_70.le0_mul [in mathcomp.algebra.ssrnum]
Num.Builders_70.le0_add [in mathcomp.algebra.ssrnum]
Num.Builders_70.sub_ge0 [in mathcomp.algebra.ssrnum]
Num.Builders_70.lt0N [in mathcomp.algebra.ssrnum]
Num.Builders_58.le_total [in mathcomp.algebra.ssrnum]
Num.Builders_58.le_normD [in mathcomp.algebra.ssrnum]
Num.Builders_58.normM [in mathcomp.algebra.ssrnum]
Num.Builders_58.le_def [in mathcomp.algebra.ssrnum]
Num.Builders_58.eq0_norm [in mathcomp.algebra.ssrnum]
Num.Builders_58.lt0_add [in mathcomp.algebra.ssrnum]
Num.Builders_50.le_total [in mathcomp.algebra.ssrnum]
Num.Builders_41.normrN [in mathcomp.algebra.ssrnum]
Num.Builders_41.normrN1 [in mathcomp.algebra.ssrnum]
Num.Builders_41.normrMn [in mathcomp.algebra.ssrnum]
Num.Builders_41.le_trans [in mathcomp.algebra.ssrnum]
Num.Builders_41.le_def' [in mathcomp.algebra.ssrnum]
Num.Builders_41.lerr [in mathcomp.algebra.ssrnum]
Num.Builders_41.ltW [in mathcomp.algebra.ssrnum]
Num.Builders_41.lt01 [in mathcomp.algebra.ssrnum]
Num.Builders_41.le01 [in mathcomp.algebra.ssrnum]
Num.Builders_41.lt_trans [in mathcomp.algebra.ssrnum]
Num.Builders_41.subr_gt0 [in mathcomp.algebra.ssrnum]
Num.Builders_41.subr_ge0 [in mathcomp.algebra.ssrnum]
Num.Builders_41.ge0_def [in mathcomp.algebra.ssrnum]
Num.Builders_41.ltrr [in mathcomp.algebra.ssrnum]
Num.Def.floor_subproof [in mathcomp.algebra.archimedean]
Num.Def.truncP [in mathcomp.algebra.archimedean]
Num.Def.trunc_itv [in mathcomp.algebra.archimedean]
Num.intArchimedean.is_intE [in mathcomp.algebra.archimedean]
Num.intArchimedean.is_natE [in mathcomp.algebra.archimedean]
Num.intArchimedean.truncP [in mathcomp.algebra.archimedean]
Num.Internals.addr_ge0 [in mathcomp.algebra.ssrnum]
Num.Internals.ger0_def [in mathcomp.algebra.ssrnum]
Num.Internals.ler01 [in mathcomp.algebra.ssrnum]
Num.Internals.le0r [in mathcomp.algebra.ssrnum]
Num.Internals.ltr01 [in mathcomp.algebra.ssrnum]
Num.Internals.nnegrE [in mathcomp.algebra.ssrnum]
Num.Internals.nneg_addr_closed [in mathcomp.algebra.ssrnum]
Num.Internals.nneg_divr_closed [in mathcomp.algebra.ssrnum]
Num.Internals.num_real [in mathcomp.algebra.ssrnum]
Num.Internals.oppr_ge0 [in mathcomp.algebra.ssrnum]
Num.Internals.pmulr_rgt0 [in mathcomp.algebra.ssrnum]
Num.Internals.poly_ivt [in mathcomp.algebra.ssrnum]
Num.Internals.posrE [in mathcomp.algebra.ssrnum]
Num.Internals.pos_divr_closed [in mathcomp.algebra.ssrnum]
Num.Internals.realE [in mathcomp.algebra.ssrnum]
Num.Internals.real_divr_closed [in mathcomp.algebra.ssrnum]
Num.Internals.real_addr_closed [in mathcomp.algebra.ssrnum]
Num.Internals.real_oppr_closed [in mathcomp.algebra.ssrnum]
Num.Internals.sqrtr_subproof [in mathcomp.algebra.ssrnum]
Num.Internals.subr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.addC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.addr_maxr [in mathcomp.algebra.ssrnum]
Num.Theory.addr_maxl [in mathcomp.algebra.ssrnum]
Num.Theory.addr_minr [in mathcomp.algebra.ssrnum]
Num.Theory.addr_minl [in mathcomp.algebra.ssrnum]
Num.Theory.addr_max_min [in mathcomp.algebra.ssrnum]
Num.Theory.addr_min_max [in mathcomp.algebra.ssrnum]
Num.Theory.addr_ss_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.addr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.archi_boundP [in mathcomp.algebra.archimedean]
Num.Theory.aut_intr [in mathcomp.algebra.archimedean]
Num.Theory.aut_natr [in mathcomp.algebra.archimedean]
Num.Theory.bigmax_real [in mathcomp.algebra.ssrnum]
Num.Theory.bigmin_real [in mathcomp.algebra.ssrnum]
Num.Theory.big_real [in mathcomp.algebra.ssrnum]
Num.Theory.Cauchy_root_bound [in mathcomp.algebra.ssrnum]
Num.Theory.ceilDrz [in mathcomp.algebra.archimedean]
Num.Theory.ceilDzr [in mathcomp.algebra.archimedean]
Num.Theory.ceilK [in mathcomp.algebra.archimedean]
Num.Theory.ceilM [in mathcomp.algebra.archimedean]
Num.Theory.ceilN [in mathcomp.algebra.archimedean]
Num.Theory.ceilX [in mathcomp.algebra.archimedean]
Num.Theory.ceil_floor [in mathcomp.algebra.archimedean]
Num.Theory.ceil_le_int [in mathcomp.algebra.archimedean]
Num.Theory.ceil_itv [in mathcomp.algebra.archimedean]
Num.Theory.ceil_le [in mathcomp.algebra.archimedean]
Num.Theory.ceil_def [in mathcomp.algebra.archimedean]
Num.Theory.ceil0 [in mathcomp.algebra.archimedean]
Num.Theory.ceil1 [in mathcomp.algebra.archimedean]
Num.Theory.char_num [in mathcomp.algebra.ssrnum]
Num.Theory.comparablerE [in mathcomp.algebra.ssrnum]
Num.Theory.comparabler_trans [in mathcomp.algebra.ssrnum]
Num.Theory.comparabler0 [in mathcomp.algebra.ssrnum]
Num.Theory.comparable0r [in mathcomp.algebra.ssrnum]
Num.Theory.conjCi [in mathcomp.algebra.ssrnum]
Num.Theory.conjCK [in mathcomp.algebra.ssrnum]
Num.Theory.conjCN1 [in mathcomp.algebra.ssrnum]
Num.Theory.conjC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.conjC_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.conjC_nat [in mathcomp.algebra.ssrnum]
Num.Theory.conjC_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.conjC0 [in mathcomp.algebra.ssrnum]
Num.Theory.conjC1 [in mathcomp.algebra.ssrnum]
Num.Theory.conj_intr [in mathcomp.algebra.archimedean]
Num.Theory.conj_natr [in mathcomp.algebra.archimedean]
Num.Theory.conj_normC [in mathcomp.algebra.ssrnum]
Num.Theory.conj_Creal [in mathcomp.algebra.ssrnum]
Num.Theory.CrealE [in mathcomp.algebra.ssrnum]
Num.Theory.CrealJ [in mathcomp.algebra.ssrnum]
Num.Theory.CrealP [in mathcomp.algebra.ssrnum]
Num.Theory.Creal_ReP [in mathcomp.algebra.ssrnum]
Num.Theory.Creal_ImP [in mathcomp.algebra.ssrnum]
Num.Theory.Creal_Im [in mathcomp.algebra.ssrnum]
Num.Theory.Creal_Re [in mathcomp.algebra.ssrnum]
Num.Theory.Crect [in mathcomp.algebra.ssrnum]
Num.Theory.deg_le2_poly_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.deg_le2_poly_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.deg_le2_poly_delta_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.deg_le2_poly_delta_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.distrC [in mathcomp.algebra.ssrnum]
Num.Theory.divC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.divC_Crect [in mathcomp.algebra.ssrnum]
Num.Theory.divr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.divr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.eqC [in mathcomp.algebra.ssrnum]
Num.Theory.eqCP [in mathcomp.algebra.ssrnum]
Num.Theory.eqC_semipolar [in mathcomp.algebra.ssrnum]
Num.Theory.eqNr [in mathcomp.algebra.ssrnum]
Num.Theory.eqrMn2r [in mathcomp.algebra.ssrnum]
Num.Theory.eqrXn2 [in mathcomp.algebra.ssrnum]
Num.Theory.eqr_sqrtC [in mathcomp.algebra.ssrnum]
Num.Theory.eqr_rootC [in mathcomp.algebra.ssrnum]
Num.Theory.eqr_sqrt [in mathcomp.algebra.ssrnum]
Num.Theory.eqr_norm2 [in mathcomp.algebra.ssrnum]
Num.Theory.eqr_norml [in mathcomp.algebra.ssrnum]
Num.Theory.eqr_normN [in mathcomp.algebra.ssrnum]
Num.Theory.eqr_norm_id [in mathcomp.algebra.ssrnum]
Num.Theory.eqr_nat [in mathcomp.algebra.ssrnum]
Num.Theory.eqr_pMn2r [in mathcomp.algebra.ssrnum]
Num.Theory.exprCK [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_odd_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_odd_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_odd_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_odd_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_even_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_even_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_even_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_even_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_egt1 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_ege1 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_ilt1 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_ile1 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.exprn_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.expr_gt1 [in mathcomp.algebra.ssrnum]
Num.Theory.expr_ge1 [in mathcomp.algebra.ssrnum]
Num.Theory.expr_lt1 [in mathcomp.algebra.ssrnum]
Num.Theory.expr_le1 [in mathcomp.algebra.ssrnum]
Num.Theory.floorDrz [in mathcomp.algebra.archimedean]
Num.Theory.floorDzr [in mathcomp.algebra.archimedean]
Num.Theory.floorK [in mathcomp.algebra.archimedean]
Num.Theory.floorM [in mathcomp.algebra.archimedean]
Num.Theory.floorN [in mathcomp.algebra.archimedean]
Num.Theory.floorP [in mathcomp.algebra.archimedean]
Num.Theory.floorpK [in mathcomp.algebra.archimedean]
Num.Theory.floorpP [in mathcomp.algebra.archimedean]
Num.Theory.floorX [in mathcomp.algebra.archimedean]
Num.Theory.floor_ge_int [in mathcomp.algebra.archimedean]
Num.Theory.floor_itv [in mathcomp.algebra.archimedean]
Num.Theory.floor_le [in mathcomp.algebra.archimedean]
Num.Theory.floor_def [in mathcomp.algebra.archimedean]
Num.Theory.floor0 [in mathcomp.algebra.archimedean]
Num.Theory.floor1 [in mathcomp.algebra.archimedean]
Num.Theory.geC0_unit_exp [in mathcomp.algebra.ssrnum]
Num.Theory.geC0_conj [in mathcomp.algebra.ssrnum]
Num.Theory.gerBl [in mathcomp.algebra.ssrnum]
Num.Theory.gerB_real [in mathcomp.algebra.ssrnum]
Num.Theory.gerDl [in mathcomp.algebra.ssrnum]
Num.Theory.gerDr [in mathcomp.algebra.ssrnum]
Num.Theory.ger_nMr [in mathcomp.algebra.ssrnum]
Num.Theory.ger_nMl [in mathcomp.algebra.ssrnum]
Num.Theory.ger_pMr [in mathcomp.algebra.ssrnum]
Num.Theory.ger_pMl [in mathcomp.algebra.ssrnum]
Num.Theory.ger_real [in mathcomp.algebra.ssrnum]
Num.Theory.ger0P [in mathcomp.algebra.ssrnum]
Num.Theory.ger0_real [in mathcomp.algebra.ssrnum]
Num.Theory.ger0_le_norm [in mathcomp.algebra.ssrnum]
Num.Theory.ger0_norm [in mathcomp.algebra.ssrnum]
Num.Theory.ger0_def [in mathcomp.algebra.ssrnum]
Num.Theory.ger1_real [in mathcomp.algebra.ssrnum]
Num.Theory.ge_floor [in mathcomp.algebra.archimedean]
Num.Theory.ge0_cp [in mathcomp.algebra.ssrnum]
Num.Theory.gtrBl [in mathcomp.algebra.ssrnum]
Num.Theory.gtrDl [in mathcomp.algebra.ssrnum]
Num.Theory.gtrDr [in mathcomp.algebra.ssrnum]
Num.Theory.gtrN [in mathcomp.algebra.ssrnum]
Num.Theory.gtr_nMr [in mathcomp.algebra.ssrnum]
Num.Theory.gtr_nMl [in mathcomp.algebra.ssrnum]
Num.Theory.gtr_pMr [in mathcomp.algebra.ssrnum]
Num.Theory.gtr_pMl [in mathcomp.algebra.ssrnum]
Num.Theory.gtr0_sg [in mathcomp.algebra.ssrnum]
Num.Theory.gtr0_real [in mathcomp.algebra.ssrnum]
Num.Theory.gtr0_le_norm [in mathcomp.algebra.ssrnum]
Num.Theory.gt_pred_ceil [in mathcomp.algebra.archimedean]
Num.Theory.gt_ge [in mathcomp.algebra.ssrnum]
Num.Theory.gt0_cp [in mathcomp.algebra.ssrnum]
Num.Theory.ieexprIn [in mathcomp.algebra.ssrnum]
Num.Theory.ieexprn_weq1 [in mathcomp.algebra.ssrnum]
Num.Theory.imaginaryCE [in mathcomp.algebra.ssrnum]
Num.Theory.ImE [in mathcomp.algebra.ssrnum]
Num.Theory.ImM [in mathcomp.algebra.ssrnum]
Num.Theory.ImMil [in mathcomp.algebra.ssrnum]
Num.Theory.ImMir [in mathcomp.algebra.ssrnum]
Num.Theory.ImMl [in mathcomp.algebra.ssrnum]
Num.Theory.ImMr [in mathcomp.algebra.ssrnum]
Num.Theory.ImV [in mathcomp.algebra.ssrnum]
Num.Theory.Im_rootC_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.Im_div [in mathcomp.algebra.ssrnum]
Num.Theory.Im_rect [in mathcomp.algebra.ssrnum]
Num.Theory.Im_conj [in mathcomp.algebra.ssrnum]
Num.Theory.Im_i [in mathcomp.algebra.ssrnum]
Num.Theory.Im_is_additive [in mathcomp.algebra.ssrnum]
Num.Theory.Im_lock [in mathcomp.algebra.ssrnum]
Num.Theory.intrE [in mathcomp.algebra.archimedean]
Num.Theory.intrEceil [in mathcomp.algebra.archimedean]
Num.Theory.intrEfloor [in mathcomp.algebra.archimedean]
Num.Theory.intrEge0 [in mathcomp.algebra.archimedean]
Num.Theory.intrEsign [in mathcomp.algebra.archimedean]
Num.Theory.intrKceil [in mathcomp.algebra.archimedean]
Num.Theory.intrKfloor [in mathcomp.algebra.archimedean]
Num.Theory.intrP [in mathcomp.algebra.archimedean]
Num.Theory.intr_aut [in mathcomp.algebra.archimedean]
Num.Theory.intr_ler_sqr [in mathcomp.algebra.archimedean]
Num.Theory.intr_normK [in mathcomp.algebra.archimedean]
Num.Theory.intr_nat [in mathcomp.algebra.archimedean]
Num.Theory.intr_int [in mathcomp.algebra.archimedean]
Num.Theory.int_num_subring [in mathcomp.algebra.archimedean]
Num.Theory.int_num1 [in mathcomp.algebra.archimedean]
Num.Theory.int_num0 [in mathcomp.algebra.archimedean]
Num.Theory.invCi [in mathcomp.algebra.ssrnum]
Num.Theory.invC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.invC_Crect [in mathcomp.algebra.ssrnum]
Num.Theory.invC_norm [in mathcomp.algebra.ssrnum]
Num.Theory.invf_lt1 [in mathcomp.algebra.ssrnum]
Num.Theory.invf_le1 [in mathcomp.algebra.ssrnum]
Num.Theory.invf_nle [in mathcomp.algebra.ssrnum]
Num.Theory.invf_nlt [in mathcomp.algebra.ssrnum]
Num.Theory.invf_ple [in mathcomp.algebra.ssrnum]
Num.Theory.invf_plt [in mathcomp.algebra.ssrnum]
Num.Theory.invf_ge1 [in mathcomp.algebra.ssrnum]
Num.Theory.invf_gt1 [in mathcomp.algebra.ssrnum]
Num.Theory.invf_nge [in mathcomp.algebra.ssrnum]
Num.Theory.invf_ngt [in mathcomp.algebra.ssrnum]
Num.Theory.invf_pge [in mathcomp.algebra.ssrnum]
Num.Theory.invf_pgt [in mathcomp.algebra.ssrnum]
Num.Theory.invr_sg [in mathcomp.algebra.ssrnum]
Num.Theory.invr_lt1 [in mathcomp.algebra.ssrnum]
Num.Theory.invr_le1 [in mathcomp.algebra.ssrnum]
Num.Theory.invr_ge1 [in mathcomp.algebra.ssrnum]
Num.Theory.invr_gt1 [in mathcomp.algebra.ssrnum]
Num.Theory.invr_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.invr_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.invr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.invr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.lef_nV2 [in mathcomp.algebra.ssrnum]
Num.Theory.lef_pV2 [in mathcomp.algebra.ssrnum]
Num.Theory.leifBLR [in mathcomp.algebra.ssrnum]
Num.Theory.leifBRL [in mathcomp.algebra.ssrnum]
Num.Theory.leifD [in mathcomp.algebra.ssrnum]
Num.Theory.leif_rootC_AGM [in mathcomp.algebra.ssrnum]
Num.Theory.leif_Re_Creal [in mathcomp.algebra.ssrnum]
Num.Theory.leif_normC_Re_Creal [in mathcomp.algebra.ssrnum]
Num.Theory.leif_AGM2 [in mathcomp.algebra.ssrnum]
Num.Theory.leif_mean_square [in mathcomp.algebra.ssrnum]
Num.Theory.leif_AGM2_scaled [in mathcomp.algebra.ssrnum]
Num.Theory.leif_mean_square_scaled [in mathcomp.algebra.ssrnum]
Num.Theory.leif_AGM [in mathcomp.algebra.ssrnum]
Num.Theory.leif_AGM_scaled [in mathcomp.algebra.ssrnum]
Num.Theory.leif_pprod [in mathcomp.algebra.ssrnum]
Num.Theory.leif_nM [in mathcomp.algebra.ssrnum]
Num.Theory.leif_pM [in mathcomp.algebra.ssrnum]
Num.Theory.leif_0_sum [in mathcomp.algebra.ssrnum]
Num.Theory.leif_sum [in mathcomp.algebra.ssrnum]
Num.Theory.leif_nat_r [in mathcomp.algebra.ssrnum]
Num.Theory.lerB [in mathcomp.algebra.ssrnum]
Num.Theory.lerBlDl [in mathcomp.algebra.ssrnum]
Num.Theory.lerBlDr [in mathcomp.algebra.ssrnum]
Num.Theory.lerBrDl [in mathcomp.algebra.ssrnum]
Num.Theory.lerBrDr [in mathcomp.algebra.ssrnum]
Num.Theory.lerB_dist [in mathcomp.algebra.ssrnum]
Num.Theory.lerB_normD [in mathcomp.algebra.ssrnum]
Num.Theory.lerB_real [in mathcomp.algebra.ssrnum]
Num.Theory.lerD [in mathcomp.algebra.ssrnum]
Num.Theory.lerDl [in mathcomp.algebra.ssrnum]
Num.Theory.lerDr [in mathcomp.algebra.ssrnum]
Num.Theory.lerD2l [in mathcomp.algebra.ssrnum]
Num.Theory.lerD2r [in mathcomp.algebra.ssrnum]
Num.Theory.lerMn2r [in mathcomp.algebra.ssrnum]
Num.Theory.lerNl [in mathcomp.algebra.ssrnum]
Num.Theory.lerNnormlW [in mathcomp.algebra.ssrnum]
Num.Theory.lerNr [in mathcomp.algebra.ssrnum]
Num.Theory.lern0 [in mathcomp.algebra.ssrnum]
Num.Theory.lern1 [in mathcomp.algebra.ssrnum]
Num.Theory.lerN10 [in mathcomp.algebra.ssrnum]
Num.Theory.lerN2 [in mathcomp.algebra.ssrnum]
Num.Theory.lerP [in mathcomp.algebra.ssrnum]
Num.Theory.lerXn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ler_sqrtC [in mathcomp.algebra.ssrnum]
Num.Theory.ler_rootC [in mathcomp.algebra.ssrnum]
Num.Theory.ler_rootCl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_sqrt [in mathcomp.algebra.ssrnum]
Num.Theory.ler_psqrt [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wsqrtr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_distlCBl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_distlBl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_distlCDr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_distlDr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_distlC [in mathcomp.algebra.ssrnum]
Num.Theory.ler_distl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_normr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_normlW [in mathcomp.algebra.ssrnum]
Num.Theory.ler_normlP [in mathcomp.algebra.ssrnum]
Num.Theory.ler_norml [in mathcomp.algebra.ssrnum]
Num.Theory.ler_norm [in mathcomp.algebra.ssrnum]
Num.Theory.ler_addgt0Pl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_addgt0Pr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivrMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivlMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivrMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_ndivlMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pdivrMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pdivlMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pdivrMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pdivlMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_nnorml [in mathcomp.algebra.ssrnum]
Num.Theory.ler_dist_normD [in mathcomp.algebra.ssrnum]
Num.Theory.ler_dist_dist [in mathcomp.algebra.ssrnum]
Num.Theory.ler_distD [in mathcomp.algebra.ssrnum]
Num.Theory.ler_normB [in mathcomp.algebra.ssrnum]
Num.Theory.ler_norm_sum [in mathcomp.algebra.ssrnum]
Num.Theory.ler_nV2 [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pV2 [in mathcomp.algebra.ssrnum]
Num.Theory.ler_sqr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pXn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ler_eXn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_iXn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_weXn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wiXn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_eXnr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_iXnr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_niMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_piMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_niMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_piMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_neMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_peMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_neMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_peMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_nMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_nMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pMr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pMl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_prod [in mathcomp.algebra.ssrnum]
Num.Theory.ler_nat [in mathcomp.algebra.ssrnum]
Num.Theory.ler_nMn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pMn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wnMn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wpMn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wMn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pMn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pM [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wnM2r [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wnM2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wpM2r [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wpM2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_nM2r [in mathcomp.algebra.ssrnum]
Num.Theory.ler_nM2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pM2r [in mathcomp.algebra.ssrnum]
Num.Theory.ler_pM2l [in mathcomp.algebra.ssrnum]
Num.Theory.ler_sum_nat [in mathcomp.algebra.ssrnum]
Num.Theory.ler_sum [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wnDr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wpDr [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wnDl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_wpDl [in mathcomp.algebra.ssrnum]
Num.Theory.ler_ltB [in mathcomp.algebra.ssrnum]
Num.Theory.ler_ltD [in mathcomp.algebra.ssrnum]
Num.Theory.ler_real [in mathcomp.algebra.ssrnum]
Num.Theory.ler_leVge [in mathcomp.algebra.ssrnum]
Num.Theory.ler0n [in mathcomp.algebra.ssrnum]
Num.Theory.ler0N1 [in mathcomp.algebra.ssrnum]
Num.Theory.ler0P [in mathcomp.algebra.ssrnum]
Num.Theory.ler0_sqrtr [in mathcomp.algebra.ssrnum]
Num.Theory.ler0_real [in mathcomp.algebra.ssrnum]
Num.Theory.ler0_ge_norm [in mathcomp.algebra.ssrnum]
Num.Theory.ler0_norm [in mathcomp.algebra.ssrnum]
Num.Theory.ler0_def [in mathcomp.algebra.ssrnum]
Num.Theory.ler01 [in mathcomp.algebra.ssrnum]
Num.Theory.ler1n [in mathcomp.algebra.ssrnum]
Num.Theory.ler1_real [in mathcomp.algebra.ssrnum]
Num.Theory.ler10 [in mathcomp.algebra.ssrnum]
Num.Theory.le_ceil [in mathcomp.algebra.archimedean]
Num.Theory.le0r [in mathcomp.algebra.ssrnum]
Num.Theory.le0_cp [in mathcomp.algebra.ssrnum]
Num.Theory.lteifBlDl [in mathcomp.algebra.ssrnum]
Num.Theory.lteifBlDr [in mathcomp.algebra.ssrnum]
Num.Theory.lteifBrDl [in mathcomp.algebra.ssrnum]
Num.Theory.lteifBrDr [in mathcomp.algebra.ssrnum]
Num.Theory.lteifD2l [in mathcomp.algebra.ssrnum]
Num.Theory.lteifD2r [in mathcomp.algebra.ssrnum]
Num.Theory.lteifNl [in mathcomp.algebra.ssrnum]
Num.Theory.lteifNr [in mathcomp.algebra.ssrnum]
Num.Theory.lteifNr0 [in mathcomp.algebra.ssrnum]
Num.Theory.lteifN2 [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_distl [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_normr [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_norml [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_ndivrMl [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_ndivlMl [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_ndivrMr [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_ndivlMr [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_pdivrMl [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_pdivlMl [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_pdivrMr [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_pdivlMr [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_nnormr [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_nM2r [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_nM2l [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_pM2r [in mathcomp.algebra.ssrnum]
Num.Theory.lteif_pM2l [in mathcomp.algebra.ssrnum]
Num.Theory.lteif0Nr [in mathcomp.algebra.ssrnum]
Num.Theory.lteif01 [in mathcomp.algebra.ssrnum]
Num.Theory.ltf_nV2 [in mathcomp.algebra.ssrnum]
Num.Theory.ltf_pV2 [in mathcomp.algebra.ssrnum]
Num.Theory.ltrB [in mathcomp.algebra.ssrnum]
Num.Theory.ltrBlDl [in mathcomp.algebra.ssrnum]
Num.Theory.ltrBlDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltrBrDl [in mathcomp.algebra.ssrnum]
Num.Theory.ltrBrDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltrD [in mathcomp.algebra.ssrnum]
Num.Theory.ltrDl [in mathcomp.algebra.ssrnum]
Num.Theory.ltrDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltrD2l [in mathcomp.algebra.ssrnum]
Num.Theory.ltrD2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltrgtP [in mathcomp.algebra.ssrnum]
Num.Theory.ltrgt0P [in mathcomp.algebra.ssrnum]
Num.Theory.ltrMn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltrNl [in mathcomp.algebra.ssrnum]
Num.Theory.ltrNnormlW [in mathcomp.algebra.ssrnum]
Num.Theory.ltrNr [in mathcomp.algebra.ssrnum]
Num.Theory.ltrn0 [in mathcomp.algebra.ssrnum]
Num.Theory.ltrn1 [in mathcomp.algebra.ssrnum]
Num.Theory.ltrN10 [in mathcomp.algebra.ssrnum]
Num.Theory.ltrN2 [in mathcomp.algebra.ssrnum]
Num.Theory.ltrP [in mathcomp.algebra.ssrnum]
Num.Theory.ltrXn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_sqrtC [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_rootC [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_rootCl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_sqrt [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_distlCBl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_distlBl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_distlCDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_distlDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_distlC [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_distl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_normr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_normlW [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_normlP [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_norml [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_ndivrMl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_ndivlMl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_ndivrMr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_ndivlMr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pdivrMl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pdivlMl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pdivrMr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pdivlMr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nnorml [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nV2 [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pV2 [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_sqr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pXn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wpXn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_eXn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_iXn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_eXnr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_iXnr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nMr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nMl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pMr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pMl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_prod_nat [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_prod [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nat [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nMn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pMn2l [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wpMn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wMn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pMn2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pM [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nM2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nM2l [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pM2r [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pM2l [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nwDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wnDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pwDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wpDr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nDl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_nwDl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wnDl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pDl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_pwDl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_wpDl [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_leB [in mathcomp.algebra.ssrnum]
Num.Theory.ltr_leD [in mathcomp.algebra.ssrnum]
Num.Theory.ltr0n [in mathcomp.algebra.ssrnum]
Num.Theory.ltr0N1 [in mathcomp.algebra.ssrnum]
Num.Theory.ltr0Sn [in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_sqrtr [in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_sg [in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_real [in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_ge_norm [in mathcomp.algebra.ssrnum]
Num.Theory.ltr0_neq0 [in mathcomp.algebra.ssrnum]
Num.Theory.ltr01 [in mathcomp.algebra.ssrnum]
Num.Theory.ltr1n [in mathcomp.algebra.ssrnum]
Num.Theory.ltr10 [in mathcomp.algebra.ssrnum]
Num.Theory.lt_succ_floor [in mathcomp.algebra.archimedean]
Num.Theory.lt_le [in mathcomp.algebra.ssrnum]
Num.Theory.lt0r [in mathcomp.algebra.ssrnum]
Num.Theory.lt0r_neq0 [in mathcomp.algebra.ssrnum]
Num.Theory.lt0_cp [in mathcomp.algebra.ssrnum]
Num.Theory.maxNr [in mathcomp.algebra.ssrnum]
Num.Theory.maxrN [in mathcomp.algebra.ssrnum]
Num.Theory.maxr_nMl [in mathcomp.algebra.ssrnum]
Num.Theory.maxr_nMr [in mathcomp.algebra.ssrnum]
Num.Theory.maxr_pMl [in mathcomp.algebra.ssrnum]
Num.Theory.maxr_pMr [in mathcomp.algebra.ssrnum]
Num.Theory.maxr_to_min [in mathcomp.algebra.ssrnum]
Num.Theory.max_real [in mathcomp.algebra.ssrnum]
Num.Theory.midf_lt [in mathcomp.algebra.ssrnum]
Num.Theory.midf_le [in mathcomp.algebra.ssrnum]
Num.Theory.minNr [in mathcomp.algebra.ssrnum]
Num.Theory.minrN [in mathcomp.algebra.ssrnum]
Num.Theory.minr_nMl [in mathcomp.algebra.ssrnum]
Num.Theory.minr_nMr [in mathcomp.algebra.ssrnum]
Num.Theory.minr_pMl [in mathcomp.algebra.ssrnum]
Num.Theory.minr_pMr [in mathcomp.algebra.ssrnum]
Num.Theory.minr_to_max [in mathcomp.algebra.ssrnum]
Num.Theory.min_real [in mathcomp.algebra.ssrnum]
Num.Theory.monic_Cauchy_bound [in mathcomp.algebra.ssrnum]
Num.Theory.mulCii [in mathcomp.algebra.ssrnum]
Num.Theory.mulC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.mulrIn [in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_wlt0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_wgt0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_wle0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulrn_wge0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sg_norm [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_Nsign_norm [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sign_norm [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sign_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sg_eqN1 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_sg_eq1 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_egt1 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ege1 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ilt1 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ile1 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ge0_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_le0_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ge0_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.mulr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.mul_conjC_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.mul_conjC_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.mul_conjC_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.naddr_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.natf_indexg [in mathcomp.algebra.ssrnum]
Num.Theory.natf_div [in mathcomp.algebra.ssrnum]
Num.Theory.natrE [in mathcomp.algebra.archimedean]
Num.Theory.natrEint [in mathcomp.algebra.archimedean]
Num.Theory.natrG_neq0 [in mathcomp.algebra.ssrnum]
Num.Theory.natrG_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.natrK [in mathcomp.algebra.archimedean]
Num.Theory.natrP [in mathcomp.algebra.archimedean]
Num.Theory.natr_aut [in mathcomp.algebra.archimedean]
Num.Theory.natr_exp_even [in mathcomp.algebra.archimedean]
Num.Theory.natr_norm_int [in mathcomp.algebra.archimedean]
Num.Theory.natr_prod_eq1 [in mathcomp.algebra.archimedean]
Num.Theory.natr_mul_eq1 [in mathcomp.algebra.archimedean]
Num.Theory.natr_sum_eq1 [in mathcomp.algebra.archimedean]
Num.Theory.natr_gt0 [in mathcomp.algebra.archimedean]
Num.Theory.natr_ge0 [in mathcomp.algebra.archimedean]
Num.Theory.natr_normK [in mathcomp.algebra.archimedean]
Num.Theory.natr_nat [in mathcomp.algebra.archimedean]
Num.Theory.natr_indexg_neq0 [in mathcomp.algebra.ssrnum]
Num.Theory.natr_indexg_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.nat_num_semiring [in mathcomp.algebra.archimedean]
Num.Theory.nat_num1 [in mathcomp.algebra.archimedean]
Num.Theory.nat_num0 [in mathcomp.algebra.archimedean]
Num.Theory.negrE [in mathcomp.algebra.ssrnum]
Num.Theory.neqr0_sign [in mathcomp.algebra.ssrnum]
Num.Theory.neq0Ci [in mathcomp.algebra.ssrnum]
Num.Theory.neq0_mulr_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulrn_rle0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulrn_rge0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulrn_rgt0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_lle0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_llt0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_lge0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_lgt0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_rle0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_rlt0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_rge0 [in mathcomp.algebra.ssrnum]
Num.Theory.nmulr_rgt0 [in mathcomp.algebra.ssrnum]
Num.Theory.nnegrE [in mathcomp.algebra.ssrnum]
Num.Theory.nonRealCi [in mathcomp.algebra.ssrnum]
Num.Theory.normCBeq [in mathcomp.algebra.ssrnum]
Num.Theory.normCDeq [in mathcomp.algebra.ssrnum]
Num.Theory.normCi [in mathcomp.algebra.ssrnum]
Num.Theory.normCKC [in mathcomp.algebra.ssrnum]
Num.Theory.normC_sum_upper [in mathcomp.algebra.ssrnum]
Num.Theory.normC_sum_eq1 [in mathcomp.algebra.ssrnum]
Num.Theory.normC_sum_eq [in mathcomp.algebra.ssrnum]
Num.Theory.normC_Re_Im [in mathcomp.algebra.ssrnum]
Num.Theory.normC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.normC_def [in mathcomp.algebra.ssrnum]
Num.Theory.normC2_Re_Im [in mathcomp.algebra.ssrnum]
Num.Theory.normC2_rect [in mathcomp.algebra.ssrnum]
Num.Theory.normfV [in mathcomp.algebra.ssrnum]
Num.Theory.normf_div [in mathcomp.algebra.ssrnum]
Num.Theory.normrEsg [in mathcomp.algebra.ssrnum]
Num.Theory.normrEsign [in mathcomp.algebra.ssrnum]
Num.Theory.normrMsign [in mathcomp.algebra.ssrnum]
Num.Theory.normrN1 [in mathcomp.algebra.ssrnum]
Num.Theory.normrV [in mathcomp.algebra.ssrnum]
Num.Theory.normrX [in mathcomp.algebra.ssrnum]
Num.Theory.normr_sg [in mathcomp.algebra.ssrnum]
Num.Theory.normr_sign [in mathcomp.algebra.ssrnum]
Num.Theory.normr_real [in mathcomp.algebra.ssrnum]
Num.Theory.normr_nneg [in mathcomp.algebra.ssrnum]
Num.Theory.normr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.normr_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.normr_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.normr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.normr_id [in mathcomp.algebra.ssrnum]
Num.Theory.normr_unit [in mathcomp.algebra.ssrnum]
Num.Theory.normr_prod [in mathcomp.algebra.ssrnum]
Num.Theory.normr_nat [in mathcomp.algebra.ssrnum]
Num.Theory.normr_idP [in mathcomp.algebra.ssrnum]
Num.Theory.normr0 [in mathcomp.algebra.ssrnum]
Num.Theory.normr0P [in mathcomp.algebra.ssrnum]
Num.Theory.normr1 [in mathcomp.algebra.ssrnum]
Num.Theory.norm_intr_ge1 [in mathcomp.algebra.archimedean]
Num.Theory.norm_natr [in mathcomp.algebra.archimedean]
Num.Theory.norm_conjC [in mathcomp.algebra.ssrnum]
Num.Theory.norm_rootC [in mathcomp.algebra.ssrnum]
Num.Theory.nposrE [in mathcomp.algebra.ssrnum]
Num.Theory.Nreal_gtF [in mathcomp.algebra.ssrnum]
Num.Theory.Nreal_ltF [in mathcomp.algebra.ssrnum]
Num.Theory.Nreal_geF [in mathcomp.algebra.ssrnum]
Num.Theory.Nreal_leF [in mathcomp.algebra.ssrnum]
Num.Theory.numEsg [in mathcomp.algebra.ssrnum]
Num.Theory.numEsign [in mathcomp.algebra.ssrnum]
Num.Theory.numNEsign [in mathcomp.algebra.ssrnum]
Num.Theory.num_real [in mathcomp.algebra.ssrnum]
Num.Theory.oppC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.oppr_min [in mathcomp.algebra.ssrnum]
Num.Theory.oppr_max [in mathcomp.algebra.ssrnum]
Num.Theory.oppr_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.oppr_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.oppr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.oppr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.paddr_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.NumClosedMonic.deg2_poly_root2 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.NumClosedMonic.deg2_poly_root1 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.NumClosedMonic.deg2_poly_factor [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.NumClosed.deg2_poly_root2 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.NumClosed.deg2_poly_root1 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.NumClosed.deg2_poly_factor [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_le0m [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_ge0r [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_ge0l [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_lt0m [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_gt0r [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_gt0l [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_noroot [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_root2 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_root1 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_factor [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_minE [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.RealMonic.deg2_poly_min [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_ge0m [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_le0r [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_le0l [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_gt0m [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_lt0r [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_lt0l [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_le0m [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_ge0r [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_ge0l [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_lt0m [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_gt0r [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_gt0l [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_noroot [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_root2 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_root1 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_factor [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_maxE [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_max [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_minE [in mathcomp.algebra.ssrnum]
Num.Theory.Pdeg2.Real.deg2_poly_min [in mathcomp.algebra.ssrnum]
Num.Theory.pexpIrn [in mathcomp.algebra.ssrnum]
Num.Theory.pexprn_eq1 [in mathcomp.algebra.ssrnum]
Num.Theory.pexpr_eq1 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulrnI [in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_rle0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_rge0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_rlt0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_rgt0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_lle0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_lge0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_llt0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulrn_lgt0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_lle0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_llt0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_lge0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_lgt0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_rle0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_rlt0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_rge0 [in mathcomp.algebra.ssrnum]
Num.Theory.pmulr_rgt0 [in mathcomp.algebra.ssrnum]
Num.Theory.pnatr_eq1 [in mathcomp.algebra.ssrnum]
Num.Theory.pnatr_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.poly_ivt [in mathcomp.algebra.ssrnum]
Num.Theory.poly_itv_bound [in mathcomp.algebra.ssrnum]
Num.Theory.poly_disk_bound [in mathcomp.algebra.ssrnum]
Num.Theory.posrE [in mathcomp.algebra.ssrnum]
Num.Theory.prodr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.prodr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.prod_truncK [in mathcomp.algebra.archimedean]
Num.Theory.prod_real [in mathcomp.algebra.ssrnum]
Num.Theory.psumr_neq0P [in mathcomp.algebra.ssrnum]
Num.Theory.psumr_neq0 [in mathcomp.algebra.ssrnum]
Num.Theory.psumr_eq0P [in mathcomp.algebra.ssrnum]
Num.Theory.psumr_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.raddfZ_int [in mathcomp.algebra.archimedean]
Num.Theory.raddfZ_nat [in mathcomp.algebra.archimedean]
Num.Theory.realB [in mathcomp.algebra.ssrnum]
Num.Theory.realBC [in mathcomp.algebra.ssrnum]
Num.Theory.realD [in mathcomp.algebra.ssrnum]
Num.Theory.realE [in mathcomp.algebra.ssrnum]
Num.Theory.realEsg [in mathcomp.algebra.ssrnum]
Num.Theory.realEsign [in mathcomp.algebra.ssrnum]
Num.Theory.realEsqr [in mathcomp.algebra.ssrnum]
Num.Theory.realM [in mathcomp.algebra.ssrnum]
Num.Theory.realMr [in mathcomp.algebra.ssrnum]
Num.Theory.realN [in mathcomp.algebra.ssrnum]
Num.Theory.realn [in mathcomp.algebra.ssrnum]
Num.Theory.realNEsign [in mathcomp.algebra.ssrnum]
Num.Theory.realn_nmono_in [in mathcomp.algebra.ssrnum]
Num.Theory.realn_mono_in [in mathcomp.algebra.ssrnum]
Num.Theory.realn_nmono [in mathcomp.algebra.ssrnum]
Num.Theory.realn_mono [in mathcomp.algebra.ssrnum]
Num.Theory.realrM [in mathcomp.algebra.ssrnum]
Num.Theory.realrMn [in mathcomp.algebra.ssrnum]
Num.Theory.realV [in mathcomp.algebra.ssrnum]
Num.Theory.realX [in mathcomp.algebra.ssrnum]
Num.Theory.real_ceil_floor [in mathcomp.algebra.archimedean]
Num.Theory.real_ceilDrz [in mathcomp.algebra.archimedean]
Num.Theory.real_ceilDzr [in mathcomp.algebra.archimedean]
Num.Theory.real_ceil_le_int [in mathcomp.algebra.archimedean]
Num.Theory.real_le_ceil [in mathcomp.algebra.archimedean]
Num.Theory.real_gt_pred_ceil [in mathcomp.algebra.archimedean]
Num.Theory.real_ceil_itv [in mathcomp.algebra.archimedean]
Num.Theory.real_floorDrz [in mathcomp.algebra.archimedean]
Num.Theory.real_floorDzr [in mathcomp.algebra.archimedean]
Num.Theory.real_floor_ge_int [in mathcomp.algebra.archimedean]
Num.Theory.real_lt_succ_floor [in mathcomp.algebra.archimedean]
Num.Theory.real_ge_floor [in mathcomp.algebra.archimedean]
Num.Theory.real_floor_itv [in mathcomp.algebra.archimedean]
Num.Theory.real_leif_AGM2 [in mathcomp.algebra.ssrnum]
Num.Theory.real_leif_mean_square [in mathcomp.algebra.ssrnum]
Num.Theory.real_nmono_in [in mathcomp.algebra.ssrnum]
Num.Theory.real_mono_in [in mathcomp.algebra.ssrnum]
Num.Theory.real_nmono [in mathcomp.algebra.ssrnum]
Num.Theory.real_mono [in mathcomp.algebra.ssrnum]
Num.Theory.real_leif_AGM2_scaled [in mathcomp.algebra.ssrnum]
Num.Theory.real_leif_mean_square_scaled [in mathcomp.algebra.ssrnum]
Num.Theory.real_lteif_distl [in mathcomp.algebra.ssrnum]
Num.Theory.real_lteif_normr [in mathcomp.algebra.ssrnum]
Num.Theory.real_lteif_norml [in mathcomp.algebra.ssrnum]
Num.Theory.real_lteifNE [in mathcomp.algebra.ssrnum]
Num.Theory.real_leif_norm [in mathcomp.algebra.ssrnum]
Num.Theory.real_mulr_Nsign_norm [in mathcomp.algebra.ssrnum]
Num.Theory.real_mulr_sign_norm [in mathcomp.algebra.ssrnum]
Num.Theory.real_normrEsign [in mathcomp.algebra.ssrnum]
Num.Theory.real_normK [in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_odd_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_odd_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_odd_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_odd_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_even_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_even_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_even_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.real_exprn_even_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_distlCBl [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_distlCBl [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_distlBl [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_distlBl [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_distlCDr [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_distlCDr [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_distlDr [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_distlDr [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_distl [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_distl [in mathcomp.algebra.ssrnum]
Num.Theory.real_lerNnormlW [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_normlW [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltrNnormlW [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_normlW [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_normr [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_normr [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_normlP [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltr_norml [in mathcomp.algebra.ssrnum]
Num.Theory.real_eqr_norm2 [in mathcomp.algebra.ssrnum]
Num.Theory.real_eqr_norml [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_normlP [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_norml [in mathcomp.algebra.ssrnum]
Num.Theory.real_ler_norm [in mathcomp.algebra.ssrnum]
Num.Theory.real_arg_maxP [in mathcomp.algebra.ssrnum]
Num.Theory.real_arg_minP [in mathcomp.algebra.ssrnum]
Num.Theory.real_minNr [in mathcomp.algebra.ssrnum]
Num.Theory.real_minrN [in mathcomp.algebra.ssrnum]
Num.Theory.real_maxNr [in mathcomp.algebra.ssrnum]
Num.Theory.real_maxrN [in mathcomp.algebra.ssrnum]
Num.Theory.real_maxr_nMl [in mathcomp.algebra.ssrnum]
Num.Theory.real_minr_nMl [in mathcomp.algebra.ssrnum]
Num.Theory.real_minr_nMr [in mathcomp.algebra.ssrnum]
Num.Theory.real_maxr_nMr [in mathcomp.algebra.ssrnum]
Num.Theory.real_addr_maxr [in mathcomp.algebra.ssrnum]
Num.Theory.real_addr_maxl [in mathcomp.algebra.ssrnum]
Num.Theory.real_addr_minr [in mathcomp.algebra.ssrnum]
Num.Theory.real_addr_minl [in mathcomp.algebra.ssrnum]
Num.Theory.real_oppr_min [in mathcomp.algebra.ssrnum]
Num.Theory.real_oppr_max [in mathcomp.algebra.ssrnum]
Num.Theory.real_wlog_ltr [in mathcomp.algebra.ssrnum]
Num.Theory.real_wlog_ler [in mathcomp.algebra.ssrnum]
Num.Theory.real_neqr_lt [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltgt0P [in mathcomp.algebra.ssrnum]
Num.Theory.real_le0P [in mathcomp.algebra.ssrnum]
Num.Theory.real_ge0P [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltgtP [in mathcomp.algebra.ssrnum]
Num.Theory.real_leNgt [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltNge [in mathcomp.algebra.ssrnum]
Num.Theory.real_ltP [in mathcomp.algebra.ssrnum]
Num.Theory.real_leP [in mathcomp.algebra.ssrnum]
Num.Theory.real_comparable [in mathcomp.algebra.ssrnum]
Num.Theory.real_leVge [in mathcomp.algebra.ssrnum]
Num.Theory.real0 [in mathcomp.algebra.ssrnum]
Num.Theory.real1 [in mathcomp.algebra.ssrnum]
Num.Theory.rectC_mull [in mathcomp.algebra.ssrnum]
Num.Theory.rectC_mulr [in mathcomp.algebra.ssrnum]
Num.Theory.ReE [in mathcomp.algebra.ssrnum]
Num.Theory.ReM [in mathcomp.algebra.ssrnum]
Num.Theory.ReMil [in mathcomp.algebra.ssrnum]
Num.Theory.ReMir [in mathcomp.algebra.ssrnum]
Num.Theory.ReMl [in mathcomp.algebra.ssrnum]
Num.Theory.ReMr [in mathcomp.algebra.ssrnum]
Num.Theory.ReV [in mathcomp.algebra.ssrnum]
Num.Theory.Re_div [in mathcomp.algebra.ssrnum]
Num.Theory.Re_rect [in mathcomp.algebra.ssrnum]
Num.Theory.Re_conj [in mathcomp.algebra.ssrnum]
Num.Theory.Re_i [in mathcomp.algebra.ssrnum]
Num.Theory.Re_is_additive [in mathcomp.algebra.ssrnum]
Num.Theory.Re_lock [in mathcomp.algebra.ssrnum]
Num.Theory.rootCK [in mathcomp.algebra.ssrnum]
Num.Theory.rootCMl [in mathcomp.algebra.ssrnum]
Num.Theory.rootCMr [in mathcomp.algebra.ssrnum]
Num.Theory.rootCpX [in mathcomp.algebra.ssrnum]
Num.Theory.rootCV [in mathcomp.algebra.ssrnum]
Num.Theory.rootCX [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_lt1 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_le1 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_gt1 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_ge1 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_eq1 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_Re_max [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_inj [in mathcomp.algebra.ssrnum]
Num.Theory.rootC_subproof [in mathcomp.algebra.ssrnum]
Num.Theory.rootC0 [in mathcomp.algebra.ssrnum]
Num.Theory.rootC1 [in mathcomp.algebra.ssrnum]
Num.Theory.root0C [in mathcomp.algebra.ssrnum]
Num.Theory.root1C [in mathcomp.algebra.ssrnum]
Num.Theory.rpredZ_int [in mathcomp.algebra.archimedean]
Num.Theory.rpredZ_nat [in mathcomp.algebra.archimedean]
Num.Theory.rpred_int_num [in mathcomp.algebra.archimedean]
Num.Theory.rpred_nat_num [in mathcomp.algebra.archimedean]
Num.Theory.Rreal_int [in mathcomp.algebra.archimedean]
Num.Theory.Rreal_nat [in mathcomp.algebra.archimedean]
Num.Theory.sgrM [in mathcomp.algebra.ssrnum]
Num.Theory.sgrMn [in mathcomp.algebra.ssrnum]
Num.Theory.sgrN [in mathcomp.algebra.ssrnum]
Num.Theory.sgrN1 [in mathcomp.algebra.ssrnum]
Num.Theory.sgrP [in mathcomp.algebra.ssrnum]
Num.Theory.sgrV [in mathcomp.algebra.ssrnum]
Num.Theory.sgrX [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_smul [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_cp0 [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_norm [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_id [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_nat [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_odd [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.sgr_def [in mathcomp.algebra.ssrnum]
Num.Theory.sgr0 [in mathcomp.algebra.ssrnum]
Num.Theory.sgr1 [in mathcomp.algebra.ssrnum]
Num.Theory.signr_inj [in mathcomp.algebra.ssrnum]
Num.Theory.signr_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.signr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.signr_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.signr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.splitr [in mathcomp.algebra.ssrnum]
Num.Theory.sqrCK [in mathcomp.algebra.ssrnum]
Num.Theory.sqrCK_P [in mathcomp.algebra.ssrnum]
Num.Theory.sqrn_eq1 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrp_eq1 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtCK [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtCM [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_inj [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtC1 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtrM [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtrP [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtrV [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr_eq0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr_sqr [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqrtr1 [in mathcomp.algebra.ssrnum]
Num.Theory.sqr_intr_ge1 [in mathcomp.algebra.archimedean]
Num.Theory.sqr_sqrtr [in mathcomp.algebra.ssrnum]
Num.Theory.sqr_norm_eq1 [in mathcomp.algebra.ssrnum]
Num.Theory.sqr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.sqr_sg [in mathcomp.algebra.ssrnum]
Num.Theory.subC_rect [in mathcomp.algebra.ssrnum]
Num.Theory.subr_lteif0r [in mathcomp.algebra.ssrnum]
Num.Theory.subr_lteifr0 [in mathcomp.algebra.ssrnum]
Num.Theory.subr_comparable0 [in mathcomp.algebra.ssrnum]
Num.Theory.subr_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.subr_le0 [in mathcomp.algebra.ssrnum]
Num.Theory.subr_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.subr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.sumr_ge0 [in mathcomp.algebra.ssrnum]
Num.Theory.sum_truncK [in mathcomp.algebra.archimedean]
Num.Theory.sum_real [in mathcomp.algebra.ssrnum]
Num.Theory.truncD [in mathcomp.algebra.archimedean]
Num.Theory.truncK [in mathcomp.algebra.archimedean]
Num.Theory.truncM [in mathcomp.algebra.archimedean]
Num.Theory.truncX [in mathcomp.algebra.archimedean]
Num.Theory.trunc_floor [in mathcomp.algebra.archimedean]
Num.Theory.trunc_gt0 [in mathcomp.algebra.archimedean]
Num.Theory.trunc_def [in mathcomp.algebra.archimedean]
Num.Theory.trunc0 [in mathcomp.algebra.archimedean]
Num.Theory.trunc0Pn [in mathcomp.algebra.archimedean]
Num.Theory.trunc1 [in mathcomp.algebra.archimedean]
Num.Theory.unitf_lt0 [in mathcomp.algebra.ssrnum]
Num.Theory.unitf_gt0 [in mathcomp.algebra.ssrnum]
Num.Theory.upper_nthrootP [in mathcomp.algebra.archimedean]
Num.Theory.ZnatP [in mathcomp.algebra.archimedean]
Num.Theory.Znat_def [in mathcomp.algebra.archimedean]
nz_row_eq0 [in mathcomp.algebra.matrix]
nz_socle [in mathcomp.character.mxrepresentation]
nz_row_mxsimple [in mathcomp.character.mxrepresentation]
nz_row_sub [in mathcomp.algebra.mxalgebra]
n_act_add [in mathcomp.solvable.primitive_action]
n_act0 [in mathcomp.solvable.primitive_action]
n_act_dtuple [in mathcomp.solvable.primitive_action]
n_act_is_action [in mathcomp.solvable.primitive_action]
n_comp_connect [in mathcomp.ssreflect.fingraph]
n_comp_closure2 [in mathcomp.ssreflect.fingraph]
n_compC [in mathcomp.ssreflect.fingraph]
| 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 | (54001 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 | (1931 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 | (1658 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 | (7199 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 | (97 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 | (15214 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 | (75 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 | (224 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 | (132 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 | (2371 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 | (2266 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 | (732 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 | (21455 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 | (647 entries) |