D (Global Index)

Files

Definitions

Lemmas

Abbreviations

Global Index

D

d [abbrev, in mathcomp.algebra.mxpoly]
d_cons [abbrev, in mathcomp.algebra.tensor]
dadd_grepr [def, in mathcomp.group_representation.character]
daddv_pi [def, in mathcomp.algebra.vector]
daddv_pi_add [prf, in mathcomp.algebra.vector]
daddv_pi_id [prf, in mathcomp.algebra.vector]
daddv_pi_proj [prf, in mathcomp.algebra.vector]
dc [abbrev, in mathcomp.boot.choice]
dchi [def, in mathcomp.group_representation.vcharacter]
dchi1 [prf, in mathcomp.group_representation.vcharacter]
dchi_ndirrE [prf, in mathcomp.group_representation.vcharacter]
dchi_vchar [prf, in mathcomp.group_representation.vcharacter]
dec_Cint_span [prf, in mathcomp.field.algnum]
dec_factor_theorem [prf, in mathcomp.algebra.poly]
dec_mx_reducible_semisimple [prf, in mathcomp.group_representation.mxrepresentation]
dec_mxsimple_exists [prf, in mathcomp.group_representation.mxrepresentation]
dec_Qint_span [prf, in mathcomp.algebra.rat]
decfield [file, in mathcomp.algebra.algebraic_hierarchy.decfield]
decidable_embedding [def, in mathcomp.field.algebraics_fundamentals]
decn_inj [prf, in mathcomp.boot.ssrnat]
decn_inj_in [prf, in mathcomp.boot.ssrnat]
DecSocleType [prf, in mathcomp.group_representation.mxrepresentation]
def_pblock [prf, in mathcomp.boot.finset]
def_pnElem [prf, in mathcomp.solvable.abelian]
defaultEncModRel [def, in mathcomp.boot.generic_quotient]
defaultEncModRelClass [def, in mathcomp.boot.generic_quotient]
DefaultProdLexiOrder [mod, in mathcomp.order.preorder]
DefaultProdLexiOrder [mod, in mathcomp.order.order]
DefaultProdOrder [mod, in mathcomp.order.preorder]
DefaultProdOrder [mod, in mathcomp.order.order]
DefaultSeqLexiOrder [mod, in mathcomp.order.preorder]
DefaultSeqLexiOrder [mod, in mathcomp.order.order]
DefaultSeqProdOrder [mod, in mathcomp.order.preorder]
DefaultSeqProdOrder [mod, in mathcomp.order.order]
DefaultTupleLexiOrder [mod, in mathcomp.order.preorder]
DefaultTupleLexiOrder [mod, in mathcomp.order.order]
DefaultTupleProdOrder [mod, in mathcomp.order.preorder]
DefaultTupleProdOrder [mod, in mathcomp.order.order]
defHgX [abbrev, in mathcomp.solvable.finmodule]
degree_irr1 [prf, in mathcomp.group_representation.mxrepresentation]
degree_mxminpoly [def, in mathcomp.algebra.mxpoly]
degree_mxminpoly_map [prf, in mathcomp.algebra.mxpoly]
degree_mxminpoly_proof [prf, in mathcomp.algebra.mxpoly]
delta_mx [def, in mathcomp.algebra.matrix]
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 [def, in mathcomp.algebra.rat]
denq_eq0 [prf, in mathcomp.algebra.rat]
denq_ge0 [def, 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]
deprecated_CanEqMixin [def, in mathcomp.boot.eqtype]
deprecated_filter_index_enum [prf, in mathcomp.boot.bigop]
deprecated_InjEqMixin [def, in mathcomp.boot.eqtype]
deprecated_PcanEqMixin [def, in mathcomp.boot.eqtype]
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_sub_rker [prf, in mathcomp.group_representation.mxrepresentation]
der1_subG [prf, in mathcomp.finite_group.fingroup]
der_abelian [prf, in mathcomp.solvable.commutator]
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_gFun [def, in mathcomp.solvable.commutator]
der_group_set [prf, in mathcomp.solvable.commutator]
der_igFun [def, in mathcomp.solvable.commutator]
der_mgFun [def, in mathcomp.solvable.commutator]
der_norm [prf, in mathcomp.solvable.commutator]
der_normal [prf, in mathcomp.solvable.commutator]
der_normalS [prf, in mathcomp.solvable.commutator]
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]
deriv [def, in mathcomp.algebra.poly]
deriv0 [prf, in mathcomp.algebra.poly]
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]
Derivation [def, in mathcomp.field.separable]
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]
derivCE [def, in mathcomp.algebra.poly]
derivD [prf, in mathcomp.algebra.poly]
derivE [def, in mathcomp.algebra.poly]
derived_at [def, in mathcomp.solvable.commutator]
derived_at_group [def, in mathcomp.solvable.commutator]
derivedP [prf, in mathcomp.solvable.nilpotent]
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]
derivn [def, 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_is_repr [prf, in mathcomp.group_representation.character]
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_repr [def, in mathcomp.group_representation.character]
det_repr_mx [def, in mathcomp.group_representation.character]
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 [def, in mathcomp.algebra.matrix]
determinant_alternate [prf, in mathcomp.algebra.matrix]
determinant_multilinear [prf, in mathcomp.algebra.matrix]
detM [prf, in mathcomp.algebra.matrix]
detRepr [def, in mathcomp.group_representation.character]
detRepr_lin_char [prf, in mathcomp.group_representation.character]
detV [prf, in mathcomp.algebra.matrix]
detZ [prf, in mathcomp.algebra.matrix]
dffun_aT [abbrev, in mathcomp.boot.finfun]
dffun_morphism [def, in mathcomp.finite_group.gproduct]
dffun_of_fprod [def, in mathcomp.boot.finfun]
dffun_of_fprod_bij [prf, in mathcomp.boot.finfun]
dffun_of_fprodK [prf, in mathcomp.boot.finfun]
dffunM [prf, in mathcomp.finite_group.gproduct]
dfinfun_of [def, in mathcomp.boot.finfun]
dfs [def, in mathcomp.boot.fingraph]
dfs_path [ind, in mathcomp.boot.fingraph]
dfs_path_ind [scheme, in mathcomp.boot.fingraph]
dfs_path_sind [scheme, in mathcomp.boot.fingraph]
dfs_pathP [prf, in mathcomp.boot.fingraph]
dfsP [prf, in mathcomp.boot.fingraph]
DfsPath [constr, in mathcomp.boot.fingraph]
dfung1 [def, in mathcomp.finite_group.gproduct]
dfung1_dflt [prf, in mathcomp.finite_group.gproduct]
dfung1_id [prf, in mathcomp.finite_group.gproduct]
dfung1_morphism [def, in mathcomp.finite_group.gproduct]
dfung1_morphM [prf, in mathcomp.finite_group.gproduct]
DFunWithIn [constr, in mathcomp.boot.eqtype]
DFunWithOut [constr, in mathcomp.boot.eqtype]
dfwith [def, in mathcomp.boot.eqtype]
dfwith_in [prf, in mathcomp.boot.eqtype]
dfwith_out [prf, in mathcomp.boot.eqtype]
dfwith_spec [ind, in mathcomp.boot.eqtype]
dfwithP [prf, in mathcomp.boot.eqtype]
diag_const_mx [prf, in mathcomp.algebra.matrix]
diag_mx [def, in mathcomp.algebra.matrix]
diag_mx_comm [prf, in mathcomp.algebra.matrix]
diag_mx_is_additive [def, 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_semi_additive [def, 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]
diagonalizable [abbrev, in mathcomp.algebra.mxred]
diagonalizable [abbrev, in mathcomp.algebra.mxpoly]
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 [abbrev, 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_in [abbrev, in mathcomp.algebra.mxred]
diagonalizable_in [abbrev, 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]
diagsqmx_ind [prf, in mathcomp.algebra.matrix]
diff_id_sh [prf, in mathcomp.solvable.burnside_app]
diff_roots [def, in mathcomp.algebra.poly]
diffmx [abbrev, in mathcomp.algebra.mxalgebra]
diffmx [mod, in mathcomp.algebra.mxalgebra]
diffmx.body [def, in mathcomp.algebra.mxalgebra]
diffmx.unlock [def, in mathcomp.algebra.mxalgebra]
diffmx_Locked [modtype, in mathcomp.algebra.mxalgebra]
diffmx_Locked.body [ax, in mathcomp.algebra.mxalgebra]
diffmx_Locked.unlock [ax, in mathcomp.algebra.mxalgebra]
diffmx_unlock_subterm [def, in mathcomp.algebra.mxalgebra]
diffmx_unlockable [def, in mathcomp.algebra.mxalgebra]
diffmxE [prf, in mathcomp.algebra.mxalgebra]
diffmxSl [prf, in mathcomp.algebra.mxalgebra]
diffv [def, in mathcomp.algebra.vector]
diffv_eq0 [prf, in mathcomp.algebra.vector]
diffvSl [prf, in mathcomp.algebra.vector]
Dihedral [constr, in mathcomp.solvable.extremal]
dihedral2_structure [prf, in mathcomp.solvable.extremal]
dihedral_classP [prf, in mathcomp.solvable.extremal]
dihedral_gtype [def, in mathcomp.solvable.extremal]
dIirr [def, in mathcomp.group_representation.vcharacter]
dim [def, in mathcomp.algebra.vector]
dim_abelemE [prf, in mathcomp.group_representation.mxabelem]
dim_algid [prf, in mathcomp.field.falgebra]
dim_aspaceOver [prf, in mathcomp.field.fieldext]
dim_baseVspace [prf, in mathcomp.field.fieldext]
dim_cfun [prf, in mathcomp.group_representation.classfun]
dim_cfun_on [prf, in mathcomp.group_representation.classfun]
dim_cfun_on_abelian [prf, in mathcomp.group_representation.classfun]
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_gt0 [def, in mathcomp.algebra.vector]
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]
dimv [def, in mathcomp.algebra.vector]
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]
dinjectiveb [def, in mathcomp.boot.fintype]
dinjectiveP [prf, in mathcomp.boot.fintype]
dinjectivePn [prf, in mathcomp.boot.fintype]
dir_iso3 [def, in mathcomp.solvable.burnside_app]
dir_iso3l [def, in mathcomp.solvable.burnside_app]
dir_iso_iso3 [prf, in mathcomp.solvable.burnside_app]
dir_s0p [prf, in mathcomp.solvable.burnside_app]
direct_product [def, in mathcomp.finite_group.gproduct]
directv [abbrev, in mathcomp.algebra.vector]
directv [abbrev, in mathcomp.algebra.vector]
directv_add_unique [prf, in mathcomp.algebra.vector]
directv_addE [prf, in mathcomp.algebra.vector]
directv_addP [prf, in mathcomp.algebra.vector]
directv_def [def, 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]
dirr [def, in mathcomp.group_representation.vcharacter]
dirr1 [def, in mathcomp.group_representation.vcharacter]
dirr_aut [prf, in mathcomp.group_representation.vcharacter]
dirr_constt [def, in mathcomp.group_representation.vcharacter]
dirr_constt_oppI [prf, in mathcomp.group_representation.vcharacter]
dirr_constt_oppl [prf, in mathcomp.group_representation.vcharacter]
dirr_constt_oppr [prf, in mathcomp.group_representation.vcharacter]
dirr_consttE [prf, in mathcomp.group_representation.vcharacter]
dirr_dchi [prf, in mathcomp.group_representation.vcharacter]
dirr_dIirr [def, in mathcomp.group_representation.vcharacter]
dirr_dIirrE [prf, in mathcomp.group_representation.vcharacter]
dirr_dIirrPE [prf, in mathcomp.group_representation.vcharacter]
dirr_inj [prf, in mathcomp.group_representation.vcharacter]
dirr_norm1 [prf, in mathcomp.group_representation.vcharacter]
dirr_opp [prf, in mathcomp.group_representation.vcharacter]
dirr_oppr_closed [prf, in mathcomp.group_representation.vcharacter]
dirr_sign [prf, in mathcomp.group_representation.vcharacter]
dirr_small_norm [prf, in mathcomp.group_representation.vcharacter]
dirrE [prf, in mathcomp.group_representation.vcharacter]
dIrrP [prf, in mathcomp.group_representation.vcharacter]
dirrP [prf, in mathcomp.group_representation.vcharacter]
disjoint [def, in mathcomp.boot.fintype]
disjoint0 [prf, in mathcomp.boot.fintype]
disjoint1 [prf, in mathcomp.boot.fintype]
disjoint_cat [prf, in mathcomp.boot.fintype]
disjoint_cons [prf, in mathcomp.boot.fintype]
disjoint_has [prf, in mathcomp.boot.fintype]
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]
disjointFl [prf, in mathcomp.boot.fintype]
disjointFr [prf, in mathcomp.boot.fintype]
disjoints1 [prf, in mathcomp.boot.finset]
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]
diso_group3 [def, in mathcomp.solvable.burnside_app]
div [file, in mathcomp.boot.div]
div0n [prf, in mathcomp.boot.div]
div0z [prf, in mathcomp.algebra.intdiv]
div1g [prf, in mathcomp.boot.monoid]
div_annihilant [def, in mathcomp.algebra.polyXY]
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_ring_mul_group_cyclic [prf, in mathcomp.solvable.cyclic]
divalg [file, in mathcomp.algebra.algebraic_hierarchy.divalg]
divg1 [prf, in mathcomp.boot.monoid]
divg1_eq [prf, in mathcomp.boot.monoid]
divg_closed [def, 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]
divgg [def, in mathcomp.boot.monoid]
divgI [prf, in mathcomp.finite_group.fingroup]
divgI [prf, in mathcomp.boot.monoid]
divgK [def, in mathcomp.boot.monoid]
divgKA [prf, in mathcomp.boot.monoid]
divgr [def, in mathcomp.finite_group.gproduct]
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 [def, 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]
divn [def, in mathcomp.boot.div]
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 [def, in mathcomp.algebra.rat]
divq_num_den [prf, in mathcomp.algebra.rat]
divq_spec [ind, in mathcomp.algebra.rat]
divqP [prf, in mathcomp.algebra.rat]
DivqSpecN [constr, in mathcomp.algebra.rat]
DivqSpecP [constr, in mathcomp.algebra.rat]
divz [def, in mathcomp.algebra.intdiv]
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]
dlsubmx [def, in mathcomp.algebra.matrix]
dlsubmx_diag [prf, in mathcomp.algebra.matrix]
dlsubmxEsub [prf, in mathcomp.algebra.matrix]
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 [def, in mathcomp.finite_group.morphism]
dom [abbrev, in mathcomp.finite_group.action]
dom_hom_invmx [prf, in mathcomp.group_representation.mxrepresentation]
dom_hom_mx [def, in mathcomp.group_representation.mxrepresentation]
dom_hom_mx_module [prf, in mathcomp.group_representation.mxrepresentation]
dom_ker [prf, in mathcomp.finite_group.morphism]
dom_qactJ [prf, in mathcomp.finite_group.action]
domP [prf, in mathcomp.finite_group.morphism]
Dot [abbrev, in mathcomp.algebra.sesquilinear]
Dot [mod, in mathcomp.algebra.sesquilinear]
Dot.axioms_ [rec, in mathcomp.algebra.sesquilinear]
Dot.class [proj, in mathcomp.algebra.sesquilinear]
Dot.clone [abbrev, in mathcomp.algebra.sesquilinear]
Dot.copy [abbrev, in mathcomp.algebra.sesquilinear]
Dot.Exports [mod, in mathcomp.algebra.sesquilinear]
Dot.on [abbrev, in mathcomp.algebra.sesquilinear]
Dot.on_ [abbrev, in mathcomp.algebra.sesquilinear]
Dot.pack_ [def, in mathcomp.algebra.sesquilinear]
Dot.phant_clone [def, in mathcomp.algebra.sesquilinear]
Dot.phant_on_ [def, in mathcomp.algebra.sesquilinear]
Dot.sesquilinear_isBilinear_mixin [proj, in mathcomp.algebra.sesquilinear]
Dot.sesquilinear_isDotProduct_mixin [proj, in mathcomp.algebra.sesquilinear]
Dot.sesquilinear_isHermitianSesquilinear_mixin [proj, in mathcomp.algebra.sesquilinear]
Dot.sort [proj, in mathcomp.algebra.sesquilinear]
Dot.type [rec, in mathcomp.algebra.sesquilinear]
DotElpiOperations [mod, in mathcomp.algebra.sesquilinear]
dotmx [def, in mathcomp.algebra.spectral]
dotmx_def [abbrev, in mathcomp.algebra.spectral]
dotmx_is_dot [prf, in mathcomp.algebra.spectral]
dotmx_is_hermitian [prf, in mathcomp.algebra.spectral]
dotmxE [prf, in mathcomp.algebra.spectral]
double [def, in mathcomp.boot.ssrnat]
double0 [prf, in mathcomp.boot.ssrnat]
double_eq0 [prf, in mathcomp.boot.ssrnat]
double_gt0 [prf, in mathcomp.boot.ssrnat]
double_inj [def, in mathcomp.boot.ssrnat]
double_pred [prf, in mathcomp.boot.ssrnat]
double_rec [def, 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]
dpair [def, in mathcomp.finite_group.perm]
dprod [abbrev, in mathcomp.finite_group.gproduct]
dprod [abbrev, in mathcomp.finite_group.gproduct]
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_Iirr [def, in mathcomp.group_representation.character]
dprod_Iirr0 [prf, in mathcomp.group_representation.character]
dprod_Iirr0l [prf, in mathcomp.group_representation.character]
dprod_Iirr0r [prf, in mathcomp.group_representation.character]
dprod_Iirr_eq0 [prf, in mathcomp.group_representation.character]
dprod_Iirr_inj [prf, in mathcomp.group_representation.character]
dprod_Iirr_onto [prf, in mathcomp.group_representation.character]
dprod_IirrC [prf, in mathcomp.group_representation.character]
dprod_IirrE [prf, in mathcomp.group_representation.character]
dprod_IirrEl [prf, in mathcomp.group_representation.character]
dprod_IirrEr [prf, in mathcomp.group_representation.character]
dprod_IirrK [prf, in mathcomp.group_representation.character]
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]
dprod_rowg [prf, in mathcomp.group_representation.mxabelem]
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]
dprodl_Iirr [def, in mathcomp.group_representation.character]
dprodl_Iirr0 [prf, in mathcomp.group_representation.character]
dprodl_Iirr_eq0 [prf, in mathcomp.group_representation.character]
dprodl_IirrE [prf, in mathcomp.group_representation.character]
dprodl_IirrK [prf, in mathcomp.group_representation.character]
dprodm [def, in mathcomp.finite_group.gproduct]
dprodm_cprod [prf, in mathcomp.finite_group.gproduct]
dprodm_eqf [prf, in mathcomp.finite_group.gproduct]
dprodm_morphism [def, 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]
dprodr_Iirr [def, in mathcomp.group_representation.character]
dprodr_Iirr0 [prf, in mathcomp.group_representation.character]
dprodr_Iirr_eq0 [prf, in mathcomp.group_representation.character]
dprodr_IirrE [prf, in mathcomp.group_representation.character]
dprodr_IirrK [prf, in mathcomp.group_representation.character]
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]
drop [def, in mathcomp.boot.seq]
drop0 [prf, in mathcomp.boot.seq]
drop1 [prf, in mathcomp.boot.seq]
drop_behead [prf, in mathcomp.boot.seq]
drop_bseq [def, in mathcomp.boot.tuple]
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_poly [def, in mathcomp.algebra.poly]
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_tuple [def, in mathcomp.boot.tuple]
drop_tupleP [prf, in mathcomp.boot.tuple]
drop_uniq [prf, in mathcomp.boot.seq]
dropEmask [prf, in mathcomp.boot.seq]
drsubmx [def, in mathcomp.algebra.matrix]
drsubmx_diag [prf, in mathcomp.algebra.matrix]
drsubmx_trig [prf, in mathcomp.algebra.matrix]
drsubmxEsub [prf, in mathcomp.algebra.matrix]
dsubmx [def, in mathcomp.algebra.matrix]
dsubmx_key [prf, in mathcomp.algebra.matrix]
dsubmxEsub [prf, in mathcomp.algebra.matrix]
dsumx_mul [prf, in mathcomp.group_representation.character]
dtuple_on [def, in mathcomp.solvable.primitive_action]
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]
Dummy [mod, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
Dummy.GRing [mod, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
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_irr1_cardG [prf, in mathcomp.group_representation.integral_char]
dvd_irr1_index_center [prf, in mathcomp.group_representation.integral_char]
dvd_mxminpoly [prf, in mathcomp.algebra.mxpoly]
dvdA [def, in mathcomp.field.algnum]
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]
dvdn [def, in mathcomp.boot.div]
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_cforder [prf, in mathcomp.group_representation.classfun]
dvdn_cforderP [prf, in mathcomp.group_representation.classfun]
dvdn_constt_Res1_irr1 [prf, in mathcomp.group_representation.inertia]
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]
dvdz [def, in mathcomp.algebra.intdiv]
dvdz0 [prf, in mathcomp.algebra.intdiv]
dvdz1 [prf, in mathcomp.algebra.intdiv]
dvdz_charf [abbrev, 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]