D (Lemmas)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
D (Lemmas)
dadd [prf, in mathcomp.analysis.derive]daddv_pi_add [prf, in mathcomp.algebra.vector]
daddv_pi_id [prf, in mathcomp.algebra.vector]
daddv_pi_proj [prf, in mathcomp.algebra.vector]
davg0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
davg_ge0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
davgD [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
dbilin [prf, in mathcomp.analysis.derive]
dcomp [prf, in mathcomp.analysis.derive]
dcst [prf, in mathcomp.analysis.derive]
dec_Cint_span [prf, in mathcomp.field.algnum]
dec_factor_theorem [prf, in mathcomp.algebra.poly]
dec_Qint_span [prf, in mathcomp.algebra.rat]
dec_segment_image [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
dec_surj_image_segment [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
dec_surj_image_segmentP [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
decide_or [prf, in mathcomp.classical.boolp]
decn_inj [prf, in mathcomp.boot.ssrnat]
decn_inj_in [prf, in mathcomp.boot.ssrnat]
decr_derive1_le0 [prf, in mathcomp.analysis.derive]
decr_derive1_le0_itv [prf, in mathcomp.analysis.derive]
decr_derive1_le0_itvNy [prf, in mathcomp.analysis.derive]
decr_derive1_le0_itvy [prf, in mathcomp.analysis.derive]
decreasing_cvg_at_left_comp [prf, in mathcomp.analysis.ftc]
decreasing_cvg_at_right_comp [prf, in mathcomp.analysis.ftc]
decreasing_ge0_integration_by_substitutiony [prf, in mathcomp.analysis.ftc]
decreasing_image_oo [prf, in mathcomp.analysis.ftc]
decreasing_itvNyo_bigcup [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
decreasing_itvoo_bigcup [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
decreasing_opp [prf, in mathcomp.analysis.sequences]
decreasing_seqP [prf, in mathcomp.analysis.sequences]
def_pblock [prf, in mathcomp.boot.finset]
def_pnElem [prf, in mathcomp.solvable.abelian]
default_key [prf, in mathcomp.finmap.finperm]
degree_mxminpoly_map [prf, in mathcomp.algebra.mxpoly]
degree_mxminpoly_proof [prf, in mathcomp.algebra.mxpoly]
delta_mx_dshift [prf, in mathcomp.algebra.matrix]
delta_mx_key [prf, in mathcomp.algebra.matrix]
delta_mx_lshift [prf, in mathcomp.algebra.matrix]
delta_mx_rshift [prf, in mathcomp.algebra.matrix]
delta_mx_ushift [prf, in mathcomp.algebra.matrix]
den_fracq [prf, in mathcomp.algebra.rat]
denom_Ratio [prf, in mathcomp.algebra.fraction]
denom_ratioP [prf, in mathcomp.algebra.fraction]
denq_eq0 [prf, in mathcomp.algebra.rat]
denq_gt0 [prf, in mathcomp.algebra.rat]
denq_int [prf, in mathcomp.algebra.rat]
denq_lt0 [prf, in mathcomp.algebra.rat]
denq_mulr_sign [prf, in mathcomp.algebra.rat]
denq_neq0 [prf, in mathcomp.algebra.rat]
denq_norm [prf, in mathcomp.algebra.rat]
denqN [prf, in mathcomp.algebra.rat]
denqP [prf, in mathcomp.algebra.rat]
denqVz [prf, in mathcomp.algebra.rat]
dense0 [prf, in mathcomp.analysis.topology_theory.topology_structure]
dense_rat [prf, in mathcomp.analysis.topology_theory.num_topology]
dense_set1C [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
denseI [prf, in mathcomp.analysis.topology_theory.topology_structure]
denseNE [prf, in mathcomp.analysis.topology_theory.topology_structure]
deprecated_filter_index_enum [prf, in mathcomp.boot.bigop]
der1_joing_cycles [prf, in mathcomp.solvable.commutator]
der1_min [prf, in mathcomp.solvable.commutator]
der1_stab_Ohm1_SCN_series [prf, in mathcomp.solvable.maximal]
der1_subG [prf, in mathcomp.finite_group.fingroup]
der_abelian [prf, in mathcomp.solvable.commutator]
der_add [prf, in mathcomp.analysis.derive]
der_bigcprod [prf, in mathcomp.solvable.nilpotent]
der_bigdprod [prf, in mathcomp.solvable.nilpotent]
der_char [prf, in mathcomp.solvable.commutator]
der_cont [prf, in mathcomp.solvable.commutator]
der_cprod [prf, in mathcomp.solvable.nilpotent]
der_dprod [prf, in mathcomp.solvable.nilpotent]
der_group_set [prf, in mathcomp.solvable.commutator]
der_inv [prf, in mathcomp.analysis.derive]
der_mult [prf, in mathcomp.analysis.derive]
der_norm [prf, in mathcomp.solvable.commutator]
der_normal [prf, in mathcomp.solvable.commutator]
der_normalS [prf, in mathcomp.solvable.commutator]
der_opp [prf, in mathcomp.analysis.derive]
der_scal [prf, in mathcomp.analysis.derive]
der_sub [prf, in mathcomp.solvable.commutator]
der_subS [prf, in mathcomp.solvable.commutator]
derg0 [prf, in mathcomp.solvable.commutator]
derg1 [prf, in mathcomp.solvable.commutator]
derG1P [prf, in mathcomp.solvable.commutator]
dergS [prf, in mathcomp.solvable.commutator]
dergSn [prf, in mathcomp.solvable.commutator]
deriv0 [prf, in mathcomp.algebra.poly]
deriv1E [prf, in mathcomp.analysis.derive]
deriv_comp [prf, in mathcomp.algebra.poly]
deriv_exp [prf, in mathcomp.algebra.poly]
deriv_is_linear [prf, in mathcomp.algebra.poly]
deriv_is_semilinear [prf, in mathcomp.algebra.poly]
deriv_map [prf, in mathcomp.algebra.poly]
deriv_mulC [prf, in mathcomp.algebra.poly]
derivable0 [prf, in mathcomp.analysis.derive]
derivable1_diffP [prf, in mathcomp.analysis.derive]
derivable1P [prf, in mathcomp.analysis.derive]
derivable_atan [prf, in mathcomp.analysis.trigo]
derivable_cos [prf, in mathcomp.analysis.trigo]
derivable_cst [prf, in mathcomp.analysis.derive]
derivable_expR [prf, in mathcomp.analysis.exp]
derivable_horner [prf, in mathcomp.analysis.derive]
derivable_id [prf, in mathcomp.analysis.derive]
derivable_max [prf, in mathcomp.analysis.derive]
derivable_min [prf, in mathcomp.analysis.derive]
derivable_mxP [prf, in mathcomp.analysis.derive]
derivable_nbhs [prf, in mathcomp.analysis.derive]
derivable_nbhsP [prf, in mathcomp.analysis.derive]
derivable_nbhsx [prf, in mathcomp.analysis.derive]
derivable_nbhsxP [prf, in mathcomp.analysis.derive]
derivable_Noy_Lcontinuous_within_itvNyc [prf, in mathcomp.analysis.realfun]
derivable_Nyo_continuousW [prf, in mathcomp.analysis.realfun]
derivable_Nyo_continuousWoo [prf, in mathcomp.analysis.realfun]
derivable_oo_continuousW [prf, in mathcomp.analysis.realfun]
derivable_oo_LRcontinuous_onemXnMr [prf, in mathcomp.analysis.probability_theory.beta_distribution]
derivable_oo_LRcontinuous_within [prf, in mathcomp.analysis.realfun]
derivable_opp [prf, in mathcomp.analysis.derive]
derivable_oy_continuousW [prf, in mathcomp.analysis.realfun]
derivable_oy_continuousWoo [prf, in mathcomp.analysis.realfun]
derivable_oy_Rcontinuous_within_itvcy [prf, in mathcomp.analysis.realfun]
derivable_powR [prf, in mathcomp.analysis.exp]
derivable_sin [prf, in mathcomp.analysis.trigo]
derivable_sum [prf, in mathcomp.analysis.derive]
derivable_tan [prf, in mathcomp.analysis.trigo]
derivable_under_integral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under]
derivable_within_continuous [prf, in mathcomp.analysis.derive]
derivableB [prf, in mathcomp.analysis.derive]
derivableD [prf, in mathcomp.analysis.derive]
derivableM [prf, in mathcomp.analysis.derive]
derivableN [prf, in mathcomp.analysis.derive]
derivableP [prf, in mathcomp.analysis.derive]
derivableV [prf, in mathcomp.analysis.derive]
derivableX [prf, in mathcomp.analysis.derive]
derivableZ [prf, in mathcomp.analysis.derive]
Derivation1 [prf, in mathcomp.field.separable]
Derivation_exp [prf, in mathcomp.field.separable]
Derivation_horner [prf, in mathcomp.field.separable]
Derivation_mul [prf, in mathcomp.field.separable]
Derivation_mul_poly [prf, in mathcomp.field.separable]
Derivation_scalar [prf, in mathcomp.field.separable]
Derivation_separable [prf, in mathcomp.field.separable]
Derivation_separableP [prf, in mathcomp.field.separable]
DerivationS [prf, in mathcomp.field.separable]
derivB [prf, in mathcomp.algebra.poly]
derivC [prf, in mathcomp.algebra.poly]
derivD [prf, in mathcomp.algebra.poly]
derivE [prf, in mathcomp.analysis.derive]
derive0 [prf, in mathcomp.analysis.derive]
derive1_at_max [prf, in mathcomp.analysis.derive]
derive1_at_min [prf, in mathcomp.analysis.derive]
derive1_atan [prf, in mathcomp.analysis.trigo]
derive1_comp [prf, in mathcomp.analysis.derive]
derive1_cst [prf, in mathcomp.analysis.derive]
derive1_exponential_pdf [prf, in mathcomp.analysis.probability_theory.exponential_distribution]
derive1_id [prf, in mathcomp.analysis.derive]
derive1_onem [prf, in mathcomp.analysis.derive]
derive1E [prf, in mathcomp.analysis.derive]
derive1E' [prf, in mathcomp.analysis.derive]
derive1Ml [prf, in mathcomp.analysis.derive]
derive1Mr [prf, in mathcomp.analysis.derive]
derive1N [prf, in mathcomp.analysis.derive]
derive1n0 [prf, in mathcomp.analysis.derive]
derive1n1 [prf, in mathcomp.analysis.derive]
derive1nS [prf, in mathcomp.analysis.derive]
derive1Sn [prf, in mathcomp.analysis.derive]
derive_cst [prf, in mathcomp.analysis.derive]
derive_expR [prf, in mathcomp.analysis.exp]
derive_id [prf, in mathcomp.analysis.derive]
derive_maxl [prf, in mathcomp.analysis.derive]
derive_maxr [prf, in mathcomp.analysis.derive]
derive_minl [prf, in mathcomp.analysis.derive]
derive_minr [prf, in mathcomp.analysis.derive]
derive_mx [prf, in mathcomp.analysis.derive]
derive_onemXn [prf, in mathcomp.analysis.probability_theory.beta_distribution]
derive_shift [prf, in mathcomp.analysis.derive]
derive_sqrt [prf, in mathcomp.analysis.realfun]
derive_sum [prf, in mathcomp.analysis.derive]
deriveB [prf, in mathcomp.analysis.derive]
deriveD [prf, in mathcomp.analysis.derive]
derivedP [prf, in mathcomp.solvable.nilpotent]
deriveE [prf, in mathcomp.analysis.derive]
deriveEjacobian [prf, in mathcomp.analysis.derive]
deriveM [prf, in mathcomp.analysis.derive]
deriveMl [prf, in mathcomp.analysis.derive]
deriveMr [prf, in mathcomp.analysis.derive]
deriveN [prf, in mathcomp.analysis.derive]
deriveV [prf, in mathcomp.analysis.derive]
deriveX [prf, in mathcomp.analysis.derive]
deriveZ [prf, in mathcomp.analysis.derive]
derivM [prf, in mathcomp.algebra.poly]
derivMn [prf, in mathcomp.algebra.poly]
derivMNn [prf, in mathcomp.algebra.poly]
derivMXaddC [prf, in mathcomp.algebra.poly]
derivMz [prf, in mathcomp.algebra.ssrint]
derivN [prf, in mathcomp.algebra.poly]
derivn0 [prf, in mathcomp.algebra.poly]
derivn1 [prf, in mathcomp.algebra.poly]
derivn_is_linear [prf, in mathcomp.algebra.poly]
derivn_is_semilinear [prf, in mathcomp.algebra.poly]
derivn_map [prf, in mathcomp.algebra.poly]
derivn_poly0 [prf, in mathcomp.algebra.poly]
derivnB [prf, in mathcomp.algebra.poly]
derivnC [prf, in mathcomp.algebra.poly]
derivnD [prf, in mathcomp.algebra.poly]
derivnMn [prf, in mathcomp.algebra.poly]
derivnMNn [prf, in mathcomp.algebra.poly]
derivnMXaddC [prf, in mathcomp.algebra.poly]
derivnN [prf, in mathcomp.algebra.poly]
derivnS [prf, in mathcomp.algebra.poly]
derivnXn [prf, in mathcomp.algebra.poly]
derivnZ [prf, in mathcomp.algebra.poly]
derivSn [prf, in mathcomp.algebra.poly]
derivX [prf, in mathcomp.algebra.poly]
derivXn [prf, in mathcomp.algebra.poly]
derivXsubC [prf, in mathcomp.algebra.poly]
derivZ [prf, in mathcomp.algebra.poly]
derJ [prf, in mathcomp.solvable.commutator]
det0 [prf, in mathcomp.algebra.matrix]
det0P [prf, in mathcomp.algebra.matrix]
det1 [prf, in mathcomp.algebra.matrix]
det_diag [prf, in mathcomp.algebra.matrix]
det_inv [prf, in mathcomp.algebra.matrix]
det_lblock [prf, in mathcomp.algebra.matrix]
det_map_mx [prf, in mathcomp.algebra.matrix]
det_mulmx [prf, in mathcomp.algebra.matrix]
det_mx00 [prf, in mathcomp.algebra.matrix]
det_mx11 [prf, in mathcomp.algebra.matrix]
det_perm [prf, in mathcomp.algebra.matrix]
det_scalar [prf, in mathcomp.algebra.matrix]
det_scalar1 [prf, in mathcomp.algebra.matrix]
det_tr [prf, in mathcomp.algebra.matrix]
det_trig [prf, in mathcomp.algebra.matrix]
det_ublock [prf, in mathcomp.algebra.matrix]
det_Vandermonde [prf, in mathcomp.algebra.matrix]
determinant_alternate [prf, in mathcomp.algebra.matrix]
determinant_multilinear [prf, in mathcomp.algebra.matrix]
detM [prf, in mathcomp.algebra.matrix]
detV [prf, in mathcomp.algebra.matrix]
detZ [prf, in mathcomp.algebra.matrix]
dffun_of_fprod_bij [prf, in mathcomp.boot.finfun]
dffun_of_fprodK [prf, in mathcomp.boot.finfun]
dffunM [prf, in mathcomp.finite_group.gproduct]
dfs_pathP [prf, in mathcomp.boot.fingraph]
dfsP [prf, in mathcomp.boot.fingraph]
dfung1_dflt [prf, in mathcomp.finite_group.gproduct]
dfung1_id [prf, in mathcomp.finite_group.gproduct]
dfung1_morphM [prf, in mathcomp.finite_group.gproduct]
dfwith_continuous [prf, in mathcomp.analysis.topology_theory.function_spaces]
dfwith_in [prf, in mathcomp.boot.eqtype]
dfwith_out [prf, in mathcomp.boot.eqtype]
dfwithin [prf, in mathcomp.classical.mathcomp_extra]
dfwithout [prf, in mathcomp.classical.mathcomp_extra]
dfwithP [prf, in mathcomp.classical.mathcomp_extra]
dfwithP [prf, in mathcomp.boot.eqtype]
diag_const_mx [prf, in mathcomp.algebra.matrix]
diag_mx_comm [prf, in mathcomp.algebra.matrix]
diag_mx_is_diag [prf, in mathcomp.algebra.matrix]
diag_mx_is_linear [prf, in mathcomp.algebra.matrix]
diag_mx_is_nmod_morphism [prf, in mathcomp.algebra.matrix]
diag_mx_is_scalable [prf, in mathcomp.algebra.matrix]
diag_mx_is_trig [prf, in mathcomp.algebra.matrix]
diag_mx_is_zmod_morphism [prf, in mathcomp.algebra.matrix]
diag_mx_key [prf, in mathcomp.algebra.matrix]
diag_mx_row [prf, in mathcomp.algebra.matrix]
diag_mx_sum_delta [prf, in mathcomp.algebra.matrix]
diag_mxC [prf, in mathcomp.algebra.matrix]
diag_mxP [prf, in mathcomp.algebra.matrix]
diag_mxrow [prf, in mathcomp.algebra.matrix]
diagmx_ind [prf, in mathcomp.algebra.matrix]
diagonalizable0 [prf, in mathcomp.algebra.mxred]
diagonalizable0 [prf, in mathcomp.algebra.mxpoly]
diagonalizable_conj_diag [prf, in mathcomp.algebra.mxred]
diagonalizable_conj_diag [prf, in mathcomp.algebra.mxpoly]
diagonalizable_diag [prf, in mathcomp.algebra.mxred]
diagonalizable_diag [prf, in mathcomp.algebra.mxpoly]
diagonalizable_for_mxminpoly [prf, in mathcomp.algebra.mxpoly]
diagonalizable_for_row_base [prf, in mathcomp.algebra.mxpoly]
diagonalizable_for_sum [prf, in mathcomp.algebra.mxpoly]
diagonalizable_forLR [prf, in mathcomp.algebra.mxpoly]
diagonalizable_forP [prf, in mathcomp.algebra.mxpoly]
diagonalizable_forPex [prf, in mathcomp.algebra.mxpoly]
diagonalizable_forPp [prf, in mathcomp.algebra.mxpoly]
diagonalizable_scalar [prf, in mathcomp.algebra.mxred]
diagonalizable_scalar [prf, in mathcomp.algebra.mxpoly]
diagonalizableP [prf, in mathcomp.algebra.mxred]
diagonalizableP [prf, in mathcomp.algebra.mxpoly]
diagonalizablePeigen [prf, in mathcomp.algebra.mxred]
diagonalizablePeigen [prf, in mathcomp.algebra.mxpoly]
diagonalP [prf, in mathcomp.classical.classical_sets]
diagsqmx_ind [prf, in mathcomp.algebra.matrix]
diff1E [prf, in mathcomp.analysis.derive]
diff_bilin [prf, in mathcomp.analysis.derive]
diff_comp [prf, in mathcomp.analysis.derive]
diff_continuous [prf, in mathcomp.analysis.derive]
diff_cst [prf, in mathcomp.analysis.derive]
diff_derivable [prf, in mathcomp.analysis.derive]
diff_eqO [prf, in mathcomp.analysis.derive]
diff_id_sh [prf, in mathcomp.solvable.burnside_app]
diff_key [prf, in mathcomp.analysis.derive]
diff_lin [prf, in mathcomp.analysis.derive]
diff_locally [prf, in mathcomp.analysis.derive]
diff_locally_converse_part1 [prf, in mathcomp.analysis.derive]
diff_locallyP [prf, in mathcomp.analysis.derive]
diff_locallyx [prf, in mathcomp.analysis.derive]
diff_locallyxC [prf, in mathcomp.analysis.derive]
diff_locallyxP [prf, in mathcomp.analysis.derive]
diff_pair [prf, in mathcomp.analysis.derive]
diff_Rinv [prf, in mathcomp.analysis.derive]
diff_unique [prf, in mathcomp.analysis.derive]
diffB [prf, in mathcomp.analysis.derive]
diffD [prf, in mathcomp.analysis.derive]
diffE [prf, in mathcomp.analysis.derive]
differentiable_bilin [prf, in mathcomp.analysis.derive]
differentiable_comp [prf, in mathcomp.analysis.derive]
differentiable_continuous [prf, in mathcomp.analysis.derive]
differentiable_coord [prf, in mathcomp.analysis.derive]
differentiable_cst [prf, in mathcomp.analysis.derive]
differentiable_lsubmx [prf, in mathcomp.analysis.derive]
differentiable_pair [prf, in mathcomp.analysis.derive]
differentiable_Rinv [prf, in mathcomp.analysis.derive]
differentiable_rsubmx [prf, in mathcomp.analysis.derive]
differentiable_subr_neq0 [prf, in mathcomp.analysis.realfun]
differentiable_sum [prf, in mathcomp.analysis.derive]
differentiableB [prf, in mathcomp.analysis.derive]
differentiableD [prf, in mathcomp.analysis.derive]
differentiableM [prf, in mathcomp.analysis.derive]
differentiableN [prf, in mathcomp.analysis.derive]
differentiableP [prf, in mathcomp.analysis.derive]
differentiableV [prf, in mathcomp.analysis.derive]
differentiableX [prf, in mathcomp.analysis.derive]
differentiableZ [prf, in mathcomp.analysis.derive]
differentiableZl [prf, in mathcomp.analysis.derive]
differentiation_under_integral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under]
diffM [prf, in mathcomp.analysis.derive]
diffmxE [prf, in mathcomp.algebra.mxalgebra]
diffmxSl [prf, in mathcomp.algebra.mxalgebra]
diffN [prf, in mathcomp.analysis.derive]
diffP [prf, in mathcomp.analysis.derive]
diffs_cos [prf, in mathcomp.analysis.trigo]
diffs_sin [prf, in mathcomp.analysis.trigo]
diffV [prf, in mathcomp.analysis.derive]
diffv_eq0 [prf, in mathcomp.algebra.vector]
diffvSl [prf, in mathcomp.algebra.vector]
diffX [prf, in mathcomp.analysis.derive]
diffZ [prf, in mathcomp.analysis.derive]
diffZl [prf, in mathcomp.analysis.derive]
dihedral2_structure [prf, in mathcomp.solvable.extremal]
dihedral_classP [prf, in mathcomp.solvable.extremal]
dim_algid [prf, in mathcomp.field.falgebra]
dim_aspaceOver [prf, in mathcomp.field.fieldext]
dim_baseVspace [prf, in mathcomp.field.fieldext]
dim_cosetv [prf, in mathcomp.field.fieldext]
dim_cosetv_unit [prf, in mathcomp.field.falgebra]
dim_Fadjoin [prf, in mathcomp.field.fieldext]
dim_field_module [prf, in mathcomp.field.fieldext]
dim_fixed_galois [prf, in mathcomp.field.galois]
dim_fixedField [prf, in mathcomp.field.galois]
dim_img_form_eq0 [prf, in mathcomp.algebra.sesquilinear]
dim_img_form_eq1 [prf, in mathcomp.algebra.sesquilinear]
dim_matrix [prf, in mathcomp.algebra.vector]
dim_polyn [prf, in mathcomp.algebra.qpoly]
dim_prodv [prf, in mathcomp.field.falgebra]
dim_refBaseField [prf, in mathcomp.field.fieldext]
dim_span [prf, in mathcomp.algebra.vector]
dim_sup_field [prf, in mathcomp.field.fieldext]
dim_vline [prf, in mathcomp.algebra.vector]
dim_vspaceOver [prf, in mathcomp.field.fieldext]
dimv0 [prf, in mathcomp.algebra.vector]
dimv1 [prf, in mathcomp.field.falgebra]
dimv_add_leqif [prf, in mathcomp.algebra.vector]
dimv_cap_compl [prf, in mathcomp.algebra.vector]
dimv_compl [prf, in mathcomp.algebra.vector]
dimv_disjoint_sum [prf, in mathcomp.algebra.vector]
dimv_eq0 [prf, in mathcomp.algebra.vector]
dimv_leq_sum [prf, in mathcomp.algebra.vector]
dimv_leqif_eq [prf, in mathcomp.algebra.vector]
dimv_leqif_sup [prf, in mathcomp.algebra.vector]
dimv_sum_cap [prf, in mathcomp.algebra.vector]
dimv_sum_leqif [prf, in mathcomp.algebra.vector]
dimvf [prf, in mathcomp.algebra.vector]
dimvS [prf, in mathcomp.algebra.vector]
dinjectiveP [prf, in mathcomp.boot.fintype]
dinjectivePn [prf, in mathcomp.boot.fintype]
dinv [prf, in mathcomp.analysis.derive]
dir_iso_iso3 [prf, in mathcomp.solvable.burnside_app]
dir_s0p [prf, in mathcomp.solvable.burnside_app]
dirac0 [prf, in mathcomp.analysis.measure_theory.dirac_measure]
diracE [prf, in mathcomp.analysis.measure_theory.dirac_measure]
diracT [prf, in mathcomp.analysis.measure_theory.dirac_measure]
directv_add_unique [prf, in mathcomp.algebra.vector]
directv_addE [prf, in mathcomp.algebra.vector]
directv_addP [prf, in mathcomp.algebra.vector]
directv_sum_independent [prf, in mathcomp.algebra.vector]
directv_sum_unique [prf, in mathcomp.algebra.vector]
directv_sumE [prf, in mathcomp.algebra.vector]
directv_sumP [prf, in mathcomp.algebra.vector]
directv_trivial [prf, in mathcomp.algebra.vector]
directvE [prf, in mathcomp.algebra.vector]
directvEgeq [prf, in mathcomp.algebra.vector]
directvP [prf, in mathcomp.algebra.vector]
discontinuity_countable [prf, in mathcomp.analysis.realfun]
discrete_closed [prf, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_cvg [prf, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_hausdorff [prf, in mathcomp.analysis.topology_theory.separation_axioms]
discrete_measurable0 [prf, in mathcomp.analysis.measure_theory.measurable_structure]
discrete_measurableC [prf, in mathcomp.analysis.measure_theory.measurable_structure]
discrete_measurableU [prf, in mathcomp.analysis.measure_theory.measurable_structure]
discrete_open [prf, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_set1 [prf, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_zero_dimension [prf, in mathcomp.analysis.topology_theory.separation_axioms]
disj_itv_Rhull [prf, in mathcomp.analysis.normedtype_theory.normed_module]
disj_set2E [prf, in mathcomp.classical.classical_sets]
disj_set2P [prf, in mathcomp.classical.classical_sets]
disj_set_some [prf, in mathcomp.classical.classical_sets]
disj_set_sym [prf, in mathcomp.classical.classical_sets]
disj_setPCl [prf, in mathcomp.classical.classical_sets]
disj_setPCr [prf, in mathcomp.classical.classical_sets]
disj_setPLR [prf, in mathcomp.classical.classical_sets]
disj_setPRL [prf, in mathcomp.classical.classical_sets]
disj_setPS [prf, in mathcomp.classical.classical_sets]
disjoint0 [prf, in mathcomp.boot.fintype]
disjoint1 [prf, in mathcomp.boot.fintype]
disjoint_caratheodoryIU [prf, in mathcomp.analysis.measure_theory.measure_extension]
disjoint_cat [prf, in mathcomp.boot.fintype]
disjoint_catfAC [prf, in mathcomp.finmap.finmap]
disjoint_catfC [prf, in mathcomp.finmap.finmap]
disjoint_catfCA [prf, in mathcomp.finmap.finmap]
disjoint_catfIs [prf, in mathcomp.finmap.finmap]
disjoint_catfsI [prf, in mathcomp.finmap.finmap]
disjoint_cons [prf, in mathcomp.boot.fintype]
disjoint_fsetI0 [prf, in mathcomp.finmap.finmap]
disjoint_fsub [prf, in mathcomp.finmap.finmap]
disjoint_has [prf, in mathcomp.boot.fintype]
disjoint_isolated_limit_point [prf, in mathcomp.analysis.topology_theory.topology_structure]
disjoint_itvxx [prf, in mathcomp.classical.set_interval]
disjoint_neitv [prf, in mathcomp.classical.set_interval]
disjoint_rays [prf, in mathcomp.classical.set_interval]
disjoint_set1l [prf, in mathcomp.boot.finset]
disjoint_set1r [prf, in mathcomp.boot.finset]
disjoint_setI0 [prf, in mathcomp.boot.finset]
disjoint_subset [prf, in mathcomp.boot.fintype]
disjoint_sym [prf, in mathcomp.boot.fintype]
disjoint_vitali_collection_partition [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
disjointFl [prf, in mathcomp.boot.fintype]
disjointFr [prf, in mathcomp.boot.fintype]
disjoints1 [prf, in mathcomp.boot.finset]
disjoints_subset [prf, in mathcomp.classical.classical_sets]
disjoints_subset [prf, in mathcomp.boot.finset]
disjointU [prf, in mathcomp.boot.fintype]
disjointU1 [prf, in mathcomp.boot.fintype]
disjointW [prf, in mathcomp.boot.fintype]
disjointWl [prf, in mathcomp.boot.fintype]
disjointWr [prf, in mathcomp.boot.fintype]
distm_lt_split [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
distm_lt_splitl [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
distm_lt_splitr [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
distribution_dRV [prf, in mathcomp.analysis.probability_theory.random_variable]
distribution_dRV_enum [prf, in mathcomp.analysis.probability_theory.random_variable]
div0n [prf, in mathcomp.boot.div]
div0z [prf, in mathcomp.algebra.intdiv]
div1e [prf, in mathcomp.reals.constructive_ereal]
div1g [prf, in mathcomp.boot.monoid]
div_annihilant_in_ideal [prf, in mathcomp.algebra.polyXY]
div_annihilant_neq0 [prf, in mathcomp.algebra.polyXY]
div_annihilantP [prf, in mathcomp.algebra.polyXY]
div_beta_fun_ge0 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
div_beta_fun_le1 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
div_ring_mul_group_cyclic [prf, in mathcomp.solvable.cyclic]
divee [prf, in mathcomp.reals.constructive_ereal]
divg1 [prf, in mathcomp.boot.monoid]
divg1_eq [prf, in mathcomp.boot.monoid]
divg_eq [prf, in mathcomp.boot.monoid]
divg_eq1 [prf, in mathcomp.boot.monoid]
divg_index [prf, in mathcomp.finite_group.fingroup]
divg_indexS [prf, in mathcomp.finite_group.fingroup]
divg_normal [prf, in mathcomp.finite_group.quotient]
divgI [prf, in mathcomp.finite_group.fingroup]
divgI [prf, in mathcomp.boot.monoid]
divgKA [prf, in mathcomp.boot.monoid]
divgr_eq [prf, in mathcomp.finite_group.gproduct]
divgr_id [prf, in mathcomp.finite_group.gproduct]
divgrM [prf, in mathcomp.finite_group.gproduct]
divgrMid [prf, in mathcomp.finite_group.gproduct]
divgrMl [prf, in mathcomp.finite_group.gproduct]
divgS [prf, in mathcomp.finite_group.fingroup]
divIg [prf, in mathcomp.boot.monoid]
divisor1 [prf, in mathcomp.boot.prime]
divisors_correct [prf, in mathcomp.boot.prime]
divisors_id [prf, in mathcomp.boot.prime]
divisors_uniq [prf, in mathcomp.boot.prime]
divKg [prf, in mathcomp.boot.monoid]
divn0 [prf, in mathcomp.boot.div]
divn1 [prf, in mathcomp.boot.div]
divn2 [prf, in mathcomp.boot.div]
divn_count_dvd [prf, in mathcomp.boot.prime]
divn_eq [prf, in mathcomp.boot.div]
divn_gt0 [prf, in mathcomp.boot.div]
divn_modl [prf, in mathcomp.boot.div]
divn_mulAC [prf, in mathcomp.boot.div]
divn_pred [prf, in mathcomp.boot.div]
divn_small [prf, in mathcomp.boot.div]
divnA [prf, in mathcomp.boot.div]
divnAC [prf, in mathcomp.boot.div]
divnB [prf, in mathcomp.boot.div]
divnBl [prf, in mathcomp.boot.div]
divnBMl [prf, in mathcomp.boot.div]
divnBr [prf, in mathcomp.boot.div]
divnD [prf, in mathcomp.boot.div]
divnDl [prf, in mathcomp.boot.div]
divnDMl [prf, in mathcomp.boot.div]
divnDr [prf, in mathcomp.boot.div]
divnK [prf, in mathcomp.boot.div]
divnMA [prf, in mathcomp.boot.div]
divnMBl [prf, in mathcomp.boot.div]
divnMDl [prf, in mathcomp.boot.div]
divnMl [prf, in mathcomp.boot.div]
divnMr [prf, in mathcomp.boot.div]
divnn [prf, in mathcomp.boot.div]
divnS [prf, in mathcomp.boot.div]
divNz_nat [prf, in mathcomp.algebra.intdiv]
divp_polyOver [prf, in mathcomp.field.fieldext]
divq_num_den [prf, in mathcomp.algebra.rat]
divqP [prf, in mathcomp.algebra.rat]
divz0 [prf, in mathcomp.algebra.intdiv]
divz1 [prf, in mathcomp.algebra.intdiv]
divz_abs [prf, in mathcomp.algebra.intdiv]
divz_eq [prf, in mathcomp.algebra.intdiv]
divz_ge0 [prf, in mathcomp.algebra.intdiv]
divz_mulAC [prf, in mathcomp.algebra.intdiv]
divz_nat [prf, in mathcomp.algebra.intdiv]
divz_small [prf, in mathcomp.algebra.intdiv]
divzA [prf, in mathcomp.algebra.intdiv]
divzAC [prf, in mathcomp.algebra.intdiv]
divzDl [prf, in mathcomp.algebra.intdiv]
divzDr [prf, in mathcomp.algebra.intdiv]
divzK [prf, in mathcomp.algebra.intdiv]
divzMA [prf, in mathcomp.algebra.intdiv]
divzMA_ge0 [prf, in mathcomp.algebra.intdiv]
divzMDl [prf, in mathcomp.algebra.intdiv]
divzMl [prf, in mathcomp.algebra.intdiv]
divzMpl [prf, in mathcomp.algebra.intdiv]
divzMpr [prf, in mathcomp.algebra.intdiv]
divzMr [prf, in mathcomp.algebra.intdiv]
divzN [prf, in mathcomp.algebra.intdiv]
divzz [prf, in mathcomp.algebra.intdiv]
dlin [prf, in mathcomp.analysis.derive]
dlsubmx_diag [prf, in mathcomp.algebra.matrix]
dlsubmxEsub [prf, in mathcomp.algebra.matrix]
dnbhs0_le [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
dnbhs0_lt [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
dnbhs_ball [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
dnbhsE [prf, in mathcomp.analysis.topology_theory.topology_structure]
dnbhsN [prf, in mathcomp.analysis.topology_theory.num_topology]
dnorm_eq0 [prf, in mathcomp.algebra.sesquilinear]
dnorm_ge0 [prf, in mathcomp.algebra.sesquilinear]
dnorm_geiff0 [prf, in mathcomp.algebra.sesquilinear]
dnorm_gt0 [prf, in mathcomp.algebra.sesquilinear]
dnormB [prf, in mathcomp.algebra.sesquilinear]
dnormD [prf, in mathcomp.algebra.sesquilinear]
dnormZ [prf, in mathcomp.algebra.sesquilinear]
DnQ_extraspecial [prf, in mathcomp.solvable.extraspecial]
DnQ_P [prf, in mathcomp.solvable.extraspecial]
DnQ_pgroup [prf, in mathcomp.solvable.extraspecial]
dom_ker [prf, in mathcomp.finite_group.morphism]
dom_qactJ [prf, in mathcomp.finite_group.action]
dom_setf [prf, in mathcomp.finmap.finmap]
domf0 [prf, in mathcomp.finmap.finmap]
domf_cat [prf, in mathcomp.finmap.finmap]
domf_filterf [prf, in mathcomp.finmap.finmap]
domf_reduce [prf, in mathcomp.finmap.finmap]
domf_rem [prf, in mathcomp.finmap.finmap]
domf_restrict [prf, in mathcomp.finmap.finmap]
dominated_by1 [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
dominated_convergence [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence]
dominated_cvg [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence]
dominated_cvg0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence]
dominated_integrable [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_dominated_convergence]
dominates_cadd [prf, in mathcomp.analysis.charge]
dominates_cscalel [prf, in mathcomp.analysis.charge]
dominates_cscaler [prf, in mathcomp.analysis.charge]
dominates_induced [prf, in mathcomp.analysis.charge]
dominates_pushforward [prf, in mathcomp.analysis.charge]
dominates_uniform_prob [prf, in mathcomp.analysis.probability_theory.uniform_distribution]
domP [prf, in mathcomp.finite_group.morphism]
dopp [prf, in mathcomp.analysis.derive]
dotmx_is_dot [prf, in mathcomp.algebra.spectral]
dotmx_is_hermitian [prf, in mathcomp.algebra.spectral]
dotmxE [prf, in mathcomp.algebra.spectral]
double0 [prf, in mathcomp.boot.ssrnat]
double_eq0 [prf, in mathcomp.boot.ssrnat]
double_gt0 [prf, in mathcomp.boot.ssrnat]
double_pred [prf, in mathcomp.boot.ssrnat]
doubleB [prf, in mathcomp.boot.ssrnat]
doubleD [prf, in mathcomp.boot.ssrnat]
doubleE [prf, in mathcomp.boot.ssrnat]
doubleK [prf, in mathcomp.boot.ssrnat]
doubleMl [prf, in mathcomp.boot.ssrnat]
doubleMr [prf, in mathcomp.boot.ssrnat]
doubleS [prf, in mathcomp.boot.ssrnat]
downK [prf, in mathcomp.reals.reals]
downP [prf, in mathcomp.classical.classical_sets]
dpair [prf, in mathcomp.analysis.derive]
dprod1g [prf, in mathcomp.finite_group.gproduct]
dprod_abelem [prf, in mathcomp.solvable.abelian]
dprod_card [prf, in mathcomp.finite_group.gproduct]
dprod_exponent [prf, in mathcomp.solvable.abelian]
dprod_homocyclic [prf, in mathcomp.solvable.abelian]
dprod_modl [prf, in mathcomp.finite_group.gproduct]
dprod_modr [prf, in mathcomp.finite_group.gproduct]
dprod_nil [prf, in mathcomp.solvable.nilpotent]
dprod_normal2 [prf, in mathcomp.finite_group.gproduct]
dprodA [prf, in mathcomp.finite_group.gproduct]
dprodC [prf, in mathcomp.finite_group.gproduct]
dprodE [prf, in mathcomp.finite_group.gproduct]
dprodEcp [prf, in mathcomp.finite_group.gproduct]
dprodEsd [prf, in mathcomp.finite_group.gproduct]
dprodEY [prf, in mathcomp.finite_group.gproduct]
dprodg1 [prf, in mathcomp.finite_group.gproduct]
dprodJ [prf, in mathcomp.finite_group.gproduct]
dprodm_cprod [prf, in mathcomp.finite_group.gproduct]
dprodm_eqf [prf, in mathcomp.finite_group.gproduct]
dprodmE [prf, in mathcomp.finite_group.gproduct]
dprodmEl [prf, in mathcomp.finite_group.gproduct]
dprodmEr [prf, in mathcomp.finite_group.gproduct]
dprodP [prf, in mathcomp.finite_group.gproduct]
dprodW [prf, in mathcomp.finite_group.gproduct]
dprodWC [prf, in mathcomp.finite_group.gproduct]
dprodWcp [prf, in mathcomp.finite_group.gproduct]
dprodWsd [prf, in mathcomp.finite_group.gproduct]
dprodWsdC [prf, in mathcomp.finite_group.gproduct]
dprodWY [prf, in mathcomp.finite_group.gproduct]
dprodYP [prf, in mathcomp.finite_group.gproduct]
drop0 [prf, in mathcomp.boot.seq]
drop1 [prf, in mathcomp.boot.seq]
drop_behead [prf, in mathcomp.boot.seq]
drop_bseqP [prf, in mathcomp.boot.tuple]
drop_cat [prf, in mathcomp.boot.seq]
drop_cons [prf, in mathcomp.boot.seq]
drop_drop [prf, in mathcomp.boot.seq]
drop_index [prf, in mathcomp.boot.seq]
drop_iota [prf, in mathcomp.boot.seq]
drop_mkseq [prf, in mathcomp.boot.seq]
drop_nseq [prf, in mathcomp.boot.seq]
drop_nth [prf, in mathcomp.boot.seq]
drop_oversize [prf, in mathcomp.boot.seq]
drop_poly0l [prf, in mathcomp.algebra.poly]
drop_poly0r [prf, in mathcomp.algebra.poly]
drop_poly_eq0 [prf, in mathcomp.algebra.poly]
drop_poly_is_linear [prf, in mathcomp.algebra.poly]
drop_poly_sum [prf, in mathcomp.algebra.poly]
drop_polyD [prf, in mathcomp.algebra.poly]
drop_polyDMXn [prf, in mathcomp.algebra.poly]
drop_polyMXn [prf, in mathcomp.algebra.poly]
drop_polyMXn_id [prf, in mathcomp.algebra.poly]
drop_polyZ [prf, in mathcomp.algebra.poly]
drop_rcons [prf, in mathcomp.boot.seq]
drop_rev [prf, in mathcomp.boot.seq]
drop_size [prf, in mathcomp.boot.seq]
drop_size_cat [prf, in mathcomp.boot.seq]
drop_sorted [prf, in mathcomp.boot.path]
drop_subseq [prf, in mathcomp.boot.seq]
drop_tupleP [prf, in mathcomp.boot.tuple]
drop_uniq [prf, in mathcomp.boot.seq]
dropEmask [prf, in mathcomp.boot.seq]
drsubmx_diag [prf, in mathcomp.algebra.matrix]
drsubmx_trig [prf, in mathcomp.algebra.matrix]
drsubmxEsub [prf, in mathcomp.algebra.matrix]
dRV_dom_enum [prf, in mathcomp.analysis.probability_theory.random_variable]
dRV_expectation [prf, in mathcomp.analysis.probability_theory.random_variable]
dscale [prf, in mathcomp.analysis.derive]
dscalel [prf, in mathcomp.analysis.derive]
dsubmx_key [prf, in mathcomp.algebra.matrix]
dsubmxEsub [prf, in mathcomp.algebra.matrix]
dtuple_on_add [prf, in mathcomp.solvable.primitive_action]
dtuple_on_add_D1 [prf, in mathcomp.solvable.primitive_action]
dtuple_on_subset [prf, in mathcomp.solvable.primitive_action]
dtuple_onP [prf, in mathcomp.solvable.primitive_action]
DualAddTheoryNumDomain.dadd0e [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_eq_pinfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_ge0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_Neq_ninfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_Neq_pinfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_ss_eq0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeA [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeAC [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeACA [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeC [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeCA [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeK [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeNy [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddey [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddNye [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddye [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dEFin_semi_additive [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dEFinB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dEFinD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dEFinE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.desum_eqNy [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.desum_eqNyP [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.desum_eqy [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.desum_eqyP [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dfin_numD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dfineB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dfineD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dfsume_ge0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dfsume_gt0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dfsume_le0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dfsume_lt0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dmule2n [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.doppeB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.doppeD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsub0e [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsube0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsube_eq [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsubee [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsubeK [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsume_ge0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsume_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsumEFin [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dual_addeE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dual_addeE_def [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dual_fsumeE [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dual_sumeE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.ednatmul_ninfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.ednatmul_pinfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.ednatmulE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.EFin_dnatmul [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.fin_num_doppeB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.fin_num_doppeD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.finite_supportNe [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.gte_dN [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.le0_mule_dfsuml [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.le0_mule_dfsumr [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.ndadde_eq0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.pdadde_eq0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.pdfsume_eq0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.realDed [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.sqredD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dadde_minl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dadde_minr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dge0_muleDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dge0_muleDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dle0_muleDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dle0_muleDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dmule_natl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dmule_natr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dmuleDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dmuleDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsube_ge0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsube_gt0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsube_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsube_lt0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsuber_gt0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsuber_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsubre_gt0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsubre_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.ge0_dsume_distrl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.ge0_dsume_distrr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gee_dDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gee_dDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dBl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dBr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.le0_dsume_distrl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.le0_dsume_distrr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_abs_dadd [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_abs_dsub [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_abs_dsum [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD2l [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD2lE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD2r [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD2rE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubel_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubel_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsuber_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsuber_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubl_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubl_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubr_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubr_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_natl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_natr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_ord [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_subfset [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_subset [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_natl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_natr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_ord [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_subfset [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_subset [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_lt_dD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_pdaddl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_pdaddr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dBlDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dBlDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dBrDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dBrDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dD2lE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dD2rE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsubel_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsubel_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsuber_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsuber_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_le_dB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_le_dD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_pdaddl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_pdaddr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_spdadder [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_spdaddre [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealField.lee_daddgt0Pr [prf, in mathcomp.reals.constructive_ereal]
dvd0C [prf, in mathcomp.field.algC]
dvd0n [prf, in mathcomp.boot.div]
dvd0z [prf, in mathcomp.algebra.intdiv]
dvd1n [prf, in mathcomp.boot.div]
dvd1z [prf, in mathcomp.algebra.intdiv]
dvd_mxminpoly [prf, in mathcomp.algebra.mxpoly]
dvdA_zmod_closed [prf, in mathcomp.field.algnum]
dvdC0 [prf, in mathcomp.field.algC]
dvdC_int [prf, in mathcomp.field.algC]
dvdC_mul2l [prf, in mathcomp.field.algC]
dvdC_mul2r [prf, in mathcomp.field.algC]
dvdC_mull [prf, in mathcomp.field.algC]
dvdC_mulr [prf, in mathcomp.field.algC]
dvdC_nat [prf, in mathcomp.field.algC]
dvdC_refl [prf, in mathcomp.field.algC]
dvdC_trans [prf, in mathcomp.field.algC]
dvdC_zmod [prf, in mathcomp.field.algC]
dvdCP [prf, in mathcomp.field.algC]
dvdCP_nat [prf, in mathcomp.field.algC]
dvdn0 [prf, in mathcomp.boot.div]
dvdn1 [prf, in mathcomp.boot.div]
dvdn2 [prf, in mathcomp.boot.div]
dvdn_add [prf, in mathcomp.boot.div]
dvdn_add_eq [prf, in mathcomp.boot.div]
dvdn_addl [prf, in mathcomp.boot.div]
dvdn_addr [prf, in mathcomp.boot.div]
dvdn_biggcdP [prf, in mathcomp.boot.bigop]
dvdn_biglcmP [prf, in mathcomp.boot.bigop]
dvdn_cardMg [prf, in mathcomp.finite_group.fingroup]
dvdn_div [prf, in mathcomp.boot.div]
dvdn_divisors [prf, in mathcomp.boot.prime]
dvdn_divLR [prf, in mathcomp.boot.div]
dvdn_divRL [prf, in mathcomp.boot.div]
dvdn_double_leq [prf, in mathcomp.boot.div]
dvdn_double_ltn [prf, in mathcomp.boot.div]
dvdn_eq [prf, in mathcomp.boot.div]
dvdn_exp [prf, in mathcomp.boot.div]
dvdn_exp2l [prf, in mathcomp.boot.div]
dvdn_exp2r [prf, in mathcomp.boot.div]
dvdn_exponent [prf, in mathcomp.solvable.abelian]
dvdn_fact [prf, in mathcomp.boot.div]
dvdn_gcd [prf, in mathcomp.boot.div]
dvdn_gcdl [prf, in mathcomp.boot.div]
dvdn_gcdr [prf, in mathcomp.boot.div]
dvdn_gt0 [prf, in mathcomp.boot.div]
dvdn_indexg [prf, in mathcomp.finite_group.fingroup]
dvdn_lcm [prf, in mathcomp.boot.div]
dvdn_lcml [prf, in mathcomp.boot.div]
dvdn_lcmr [prf, in mathcomp.boot.div]
dvdn_leq [prf, in mathcomp.boot.div]
dvdn_leq_log [prf, in mathcomp.boot.prime]
dvdn_morphim [prf, in mathcomp.finite_group.quotient]
dvdn_mul [prf, in mathcomp.boot.div]
dvdn_mull [prf, in mathcomp.boot.div]
dvdn_mulr [prf, in mathcomp.boot.div]
dvdn_odd [prf, in mathcomp.boot.div]
dvdn_orbit [prf, in mathcomp.finite_group.action]
dvdn_orderC [prf, in mathcomp.field.algnum]
dvdn_part [prf, in mathcomp.boot.prime]
dvdn_partP [prf, in mathcomp.boot.prime]
dvdn_Pexp2l [prf, in mathcomp.boot.div]
dvdn_pexp2r [prf, in mathcomp.boot.div]
dvdn_pfactor [prf, in mathcomp.boot.prime]
dvdn_pmul2l [prf, in mathcomp.boot.div]
dvdn_pmul2r [prf, in mathcomp.boot.div]
dvdn_pred_predX [prf, in mathcomp.boot.binomial]
dvdn_prim_root [prf, in mathcomp.algebra.poly]
dvdn_prime2 [prf, in mathcomp.boot.prime]
dvdn_prime_cyclic [prf, in mathcomp.solvable.cyclic]
dvdn_quotient [prf, in mathcomp.finite_group.quotient]
dvdn_sub [prf, in mathcomp.boot.div]
dvdn_subl [prf, in mathcomp.boot.div]
dvdn_subr [prf, in mathcomp.boot.div]
dvdn_sum [prf, in mathcomp.boot.prime]
dvdn_trans [prf, in mathcomp.boot.div]
dvdnn [prf, in mathcomp.boot.div]
dvdnP [prf, in mathcomp.boot.div]
dvdp_order [prf, in mathcomp.field.qfpoly]
dvdp_rat_int [prf, in mathcomp.algebra.rat]
dvdp_separable [prf, in mathcomp.field.separable]
dvdpP_int [prf, in mathcomp.algebra.intdiv]
dvdpP_rat_int [prf, in mathcomp.algebra.rat]
dvdz0 [prf, in mathcomp.algebra.intdiv]
dvdz1 [prf, in mathcomp.algebra.intdiv]
dvdz_contents [prf, in mathcomp.algebra.intdiv]
dvdz_eq [prf, in mathcomp.algebra.intdiv]
dvdz_exp [prf, in mathcomp.algebra.intdiv]
dvdz_exp2l [prf, in mathcomp.algebra.intdiv]
dvdz_exp2r [prf, in mathcomp.algebra.intdiv]
dvdz_gcd [prf, in mathcomp.algebra.intdiv]
dvdz_gcdl [prf, in mathcomp.algebra.intdiv]
dvdz_gcdr [prf, in mathcomp.algebra.intdiv]
dvdz_lcm [prf, in mathcomp.algebra.intdiv]
dvdz_lcml [prf, in mathcomp.algebra.intdiv]
dvdz_lcmr [prf, in mathcomp.algebra.intdiv]
dvdz_mod0P [prf, in mathcomp.algebra.intdiv]
dvdz_mul [prf, in mathcomp.algebra.intdiv]
dvdz_mul2l [prf, in mathcomp.algebra.intdiv]
dvdz_mul2r [prf, in mathcomp.algebra.intdiv]
dvdz_mull [prf, in mathcomp.algebra.intdiv]
dvdz_mulr [prf, in mathcomp.algebra.intdiv]
dvdz_pcharf [prf, in mathcomp.algebra.intdiv]
dvdz_Pexp2l [prf, in mathcomp.algebra.intdiv]
dvdz_pexp2r [prf, in mathcomp.algebra.intdiv]
dvdz_trans [prf, in mathcomp.algebra.intdiv]
dvdz_zmod_closed [prf, in mathcomp.algebra.intdiv]
dvdzE [prf, in mathcomp.algebra.intdiv]
dvdzP [prf, in mathcomp.algebra.intdiv]
dvdzz [prf, in mathcomp.algebra.intdiv]
dvg_approx [prf, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
dvg_harmonic [prf, in mathcomp.analysis.sequences]
dvg_inP [prf, in mathcomp.classical.filter]
dvg_nseries [prf, in mathcomp.analysis.sequences]
dvg_riemannR [prf, in mathcomp.analysis.exp]
dvgP [prf, in mathcomp.classical.filter]
dyadic_itv_image [prf, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
dyadic_itv_subU [prf, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
dynkin_induction [prf, in mathcomp.analysis.measure_theory.measurable_structure]
dynkin_lambda_system [prf, in mathcomp.analysis.measure_theory.measurable_structure]
dynkin_setI_sigma_algebra [prf, in mathcomp.analysis.measure_theory.measurable_structure]
dynkinC [prf, in mathcomp.analysis.measure_theory.measurable_structure]
dynkinT [prf, in mathcomp.analysis.measure_theory.measurable_structure]
dynkinU [prf, in mathcomp.analysis.measure_theory.measurable_structure]