D (Definitions)

Files

X

Y

_

Definitions

_

Lemmas

Abbreviations

Y

_

Global Index

D (Definitions)

daddv_pi [def, in mathcomp.algebra.vector]
davg [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
decidable_embedding [def, in mathcomp.field.algebraics_fundamentals]
decode [def, in mathcomp.reals.constructive_ereal]
defaultEncModRel [def, in mathcomp.boot.generic_quotient]
defaultEncModRelClass [def, in mathcomp.boot.generic_quotient]
dEFin [def, in mathcomp.reals.constructive_ereal]
degree_mxminpoly [def, in mathcomp.algebra.mxpoly]
delta_mx [def, in mathcomp.algebra.matrix]
denq [def, in mathcomp.algebra.rat]
denq_ge0 [def, in mathcomp.algebra.rat]
dense [def, in mathcomp.analysis.topology_theory.topology_structure]
deprecated_CanEqMixin [def, in mathcomp.boot.eqtype]
deprecated_InjEqMixin [def, in mathcomp.boot.eqtype]
deprecated_PcanEqMixin [def, in mathcomp.boot.eqtype]
der_gFun [def, in mathcomp.solvable.commutator]
der_igFun [def, in mathcomp.solvable.commutator]
der_mgFun [def, in mathcomp.solvable.commutator]
deriv [def, in mathcomp.algebra.poly]
derivable [def, in mathcomp.analysis.derive]
derivable_Nyo_Lcontinuous [def, in mathcomp.analysis.realfun]
derivable_oo_LRcontinuous [def, in mathcomp.analysis.realfun]
derivable_oy_Rcontinuous [def, in mathcomp.analysis.realfun]
Derivation [def, in mathcomp.field.separable]
derivCE [def, in mathcomp.algebra.poly]
derive [def, in mathcomp.analysis.derive]
derivE [def, in mathcomp.algebra.poly]
derive1 [def, in mathcomp.analysis.derive]
derive1n [def, in mathcomp.analysis.derive]
derived_at [def, in mathcomp.solvable.commutator]
derived_at_group [def, in mathcomp.solvable.commutator]
derivn [def, in mathcomp.algebra.poly]
determinant [def, in mathcomp.algebra.matrix]
dffun_morphism [def, in mathcomp.finite_group.gproduct]
dffun_of_fprod [def, in mathcomp.boot.finfun]
dfinfun_of [def, in mathcomp.boot.finfun]
dfs [def, in mathcomp.boot.fingraph]
dfung1 [def, in mathcomp.finite_group.gproduct]
dfung1_morphism [def, in mathcomp.finite_group.gproduct]
dfwith [def, in mathcomp.classical.mathcomp_extra]
dfwith [def, in mathcomp.boot.eqtype]
diag_mx [def, in mathcomp.algebra.matrix]
diag_mx_is_additive [def, in mathcomp.algebra.matrix]
diag_mx_is_semi_additive [def, in mathcomp.algebra.matrix]
diagonal [def, in mathcomp.classical.classical_sets]
diff [def, in mathcomp.analysis.derive]
diff_roots [def, in mathcomp.algebra.poly]
diffmx.body [def, in mathcomp.algebra.mxalgebra]
diffmx.unlock [def, in mathcomp.algebra.mxalgebra]
diffmx_unlock_subterm [def, in mathcomp.algebra.mxalgebra]
diffmx_unlockable [def, in mathcomp.algebra.mxalgebra]
diffv [def, in mathcomp.algebra.vector]
dihedral_gtype [def, in mathcomp.solvable.extremal]
dim [def, in mathcomp.algebra.vector]
dim_gt0 [def, in mathcomp.algebra.vector]
dimv [def, in mathcomp.algebra.vector]
dinjectiveb [def, in mathcomp.boot.fintype]
dir_iso3 [def, in mathcomp.solvable.burnside_app]
dir_iso3l [def, in mathcomp.solvable.burnside_app]
dirac [def, in mathcomp.analysis.measure_theory.dirac_measure]
direct_product [def, in mathcomp.finite_group.gproduct]
directv_def [def, in mathcomp.algebra.vector]
discontinuity [def, in mathcomp.analysis.realfun]
discrete_ball [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_ent [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_measurable [def, in mathcomp.analysis.measure_theory.measurable_structure]
Discrete_ofNbhs.identity_builder [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.identity_builder [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.identity_builder [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_random_variable [def, in mathcomp.analysis.probability_theory.random_variable]
discrete_topology [def, in mathcomp.analysis.topology_theory.discrete_topology]
discreteMeasurableFun.pack_ [def, in mathcomp.analysis.probability_theory.random_variable]
discreteMeasurableFun.phant_clone [def, in mathcomp.analysis.probability_theory.random_variable]
discreteMeasurableFun.phant_on_ [def, in mathcomp.analysis.probability_theory.random_variable]
DiscreteNbhs.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_DistrLattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_JoinSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_Lattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_MeetSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_POrder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_Preorder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_order_topology_POrderedNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_order_topology_POrderedTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_Total [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_DistrLattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_JoinSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_Lattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_MeetSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_POrder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_Preorder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_order_topology_POrderedNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_order_topology_POrderedTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_Total [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.join_discrete_topology_DiscretePseudoMetric_between_discrete_topology_DiscreteNbhs_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.join_discrete_topology_DiscretePseudoMetric_between_discrete_topology_DiscreteTopology_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.join_discrete_topology_DiscretePseudoMetric_between_discrete_topology_DiscreteUniform_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.join_discrete_topology_DiscreteTopology_between_discrete_topology_DiscreteNbhs_and_topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.join_discrete_topology_DiscreteUniform_between_discrete_topology_DiscreteNbhs_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.join_discrete_topology_DiscreteUniform_between_discrete_topology_DiscreteTopology_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
disj_set [def, in mathcomp.classical.classical_sets]
disjoint [def, in mathcomp.boot.fintype]
disjoint_itv [def, in mathcomp.classical.set_interval]
diso_group3 [def, in mathcomp.solvable.burnside_app]
distribution [def, in mathcomp.analysis.probability_theory.random_variable]
div_annihilant [def, in mathcomp.algebra.polyXY]
div_beta_fun [def, in mathcomp.analysis.probability_theory.beta_distribution]
divg_closed [def, in mathcomp.boot.monoid]
divgg [def, in mathcomp.boot.monoid]
divgK [def, in mathcomp.boot.monoid]
divgr [def, in mathcomp.finite_group.gproduct]
divisors [def, in mathcomp.boot.prime]
divn [def, in mathcomp.boot.div]
divq [def, in mathcomp.algebra.rat]
divz [def, in mathcomp.algebra.intdiv]
dlsubmx [def, in mathcomp.algebra.matrix]
dnbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
dnbhs_filter_on [def, in mathcomp.analysis.topology_theory.topology_structure]
dom [def, in mathcomp.finite_group.morphism]
dominated_by [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
Dot.pack_ [def, in mathcomp.algebra.sesquilinear]
Dot.phant_clone [def, in mathcomp.algebra.sesquilinear]
Dot.phant_on_ [def, in mathcomp.algebra.sesquilinear]
dotmx [def, in mathcomp.algebra.spectral]
double [def, in mathcomp.boot.ssrnat]
double_inj [def, in mathcomp.boot.ssrnat]
double_rec [def, in mathcomp.boot.ssrnat]
double_snum [def, in mathcomp.reals.signed]
down [def, in mathcomp.classical.classical_sets]
dpair [def, in mathcomp.finite_group.perm]
dprodm [def, in mathcomp.finite_group.gproduct]
dprodm_morphism [def, in mathcomp.finite_group.gproduct]
drop [def, in mathcomp.boot.seq]
drop_bseq [def, in mathcomp.boot.tuple]
drop_poly [def, in mathcomp.algebra.poly]
drop_tuple [def, in mathcomp.boot.tuple]
drsubmx [def, in mathcomp.algebra.matrix]
dRV_dom [def, in mathcomp.analysis.probability_theory.random_variable]
dRV_enum [def, in mathcomp.analysis.probability_theory.random_variable]
dsubmx [def, in mathcomp.algebra.matrix]
dtuple_on [def, in mathcomp.solvable.primitive_action]
dual_adde [def, in mathcomp.reals.constructive_ereal]
dual_extended [def, in mathcomp.reals.constructive_ereal]
dvdA [def, in mathcomp.field.algnum]
dvdn [def, in mathcomp.boot.div]
dvdz [def, in mathcomp.algebra.intdiv]
dyadic_approx [def, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
dyadic_itv [def, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
dynkin [def, in mathcomp.analysis.measure_theory.measurable_structure]