| Global Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(23836 entries) | -
| Notation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1409 entries) | -
| Module Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(221 entries) | -
| Variable Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3574 entries) | -
| Library Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(90 entries) | -
| Lemma Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(12096 entries) | -
| Constructor Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(368 entries) | -
| Axiom Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(45 entries) | -
| Inductive Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(107 entries) | -
| Projection Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(273 entries) | -
| Section Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1140 entries) | -
| Abbreviation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(728 entries) | -
| Definition Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3596 entries) | -
| Record Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(189 entries) | -
D
-d [abbreviation, in mathcomp.algebra.mxpoly]-daddv_pi_add [lemma, in mathcomp.algebra.vector]
-daddv_pi_proj [lemma, in mathcomp.algebra.vector]
-daddv_pi_id [lemma, in mathcomp.algebra.vector]
-daddv_pi [definition, in mathcomp.algebra.vector]
-dadd_grepr [definition, in mathcomp.character.character]
-dc [abbreviation, in mathcomp.ssreflect.choice]
-dchi [definition, in mathcomp.character.vcharacter]
-dchi_vchar [lemma, in mathcomp.character.vcharacter]
-dchi_ndirrE [lemma, in mathcomp.character.vcharacter]
-dchi1 [lemma, in mathcomp.character.vcharacter]
-DecField [section, in mathcomp.algebra.poly]
-DecField.F [variable, in mathcomp.algebra.poly]
-decidable_embedding [definition, in mathcomp.field.algebraics_fundamentals]
-DecideRed [section, in mathcomp.character.mxrepresentation]
-DecideRed.Definitions [section, in mathcomp.character.mxrepresentation]
-DecideRed.Definitions.F [variable, in mathcomp.character.mxrepresentation]
-DecideRed.Definitions.G [variable, in mathcomp.character.mxrepresentation]
-DecideRed.Definitions.gT [variable, in mathcomp.character.mxrepresentation]
-DecideRed.Definitions.n [variable, in mathcomp.character.mxrepresentation]
-DecideRed.Definitions.rG [variable, in mathcomp.character.mxrepresentation]
-DecideRed.F [variable, in mathcomp.character.mxrepresentation]
-DecideRed.G [variable, in mathcomp.character.mxrepresentation]
-DecideRed.gT [variable, in mathcomp.character.mxrepresentation]
-DecideRed.n [variable, in mathcomp.character.mxrepresentation]
-DecideRed.rG [variable, in mathcomp.character.mxrepresentation]
-decrn_inj_in [lemma, in mathcomp.ssreflect.ssrnat]
-decrn_inj [lemma, in mathcomp.ssreflect.ssrnat]
-DecSocleType [lemma, in mathcomp.character.mxrepresentation]
-dec_mx_reducible_semisimple [lemma, in mathcomp.character.mxrepresentation]
-dec_mxsimple_exists [lemma, in mathcomp.character.mxrepresentation]
-dec_Qint_span [lemma, in mathcomp.algebra.intdiv]
-dec_Cint_span [lemma, in mathcomp.field.algnum]
-dec_factor_theorem [lemma, in mathcomp.algebra.poly]
-Def [section, in mathcomp.ssreflect.tuple]
-Def [section, in mathcomp.ssreflect.finfun]
-defaultEncModRelClass [definition, in mathcomp.ssreflect.generic_quotient]
-DefaultEncodingModuloRel [section, in mathcomp.ssreflect.generic_quotient]
-DefaultEncodingModuloRel.D [variable, in mathcomp.ssreflect.generic_quotient]
-DefaultEncodingModuloRel.r [variable, in mathcomp.ssreflect.generic_quotient]
-defHgX [abbreviation, in mathcomp.solvable.finmodule]
-Definitions [section, in mathcomp.solvable.frobenius]
-Definitions.FrobeniusAction [section, in mathcomp.solvable.frobenius]
-Definitions.FrobeniusAction.G [variable, in mathcomp.solvable.frobenius]
-Definitions.FrobeniusAction.H [variable, in mathcomp.solvable.frobenius]
-Definitions.FrobeniusAction.S [variable, in mathcomp.solvable.frobenius]
-Definitions.FrobeniusAction.sT [variable, in mathcomp.solvable.frobenius]
-Definitions.FrobeniusAction.to [variable, in mathcomp.solvable.frobenius]
-Definitions.gT [variable, in mathcomp.solvable.frobenius]
-Defs [section, in mathcomp.fingroup.gproduct]
-Defs [section, in mathcomp.solvable.maximal]
-Defs [section, in mathcomp.character.classfun]
-Defs [section, in mathcomp.solvable.center]
-Defs.Automorphism [section, in mathcomp.character.classfun]
-Defs.Automorphism.u [variable, in mathcomp.character.classfun]
-Defs.B [variable, in mathcomp.character.classfun]
-Defs.gT [variable, in mathcomp.fingroup.gproduct]
-Defs.gT [variable, in mathcomp.solvable.maximal]
-Defs.gT [variable, in mathcomp.character.classfun]
-Defs.gT [variable, in mathcomp.solvable.center]
-'1_ _ (ring_scope) [notation, in mathcomp.character.classfun]
-def_pnElem [lemma, in mathcomp.solvable.abelian]
-def_pblock [lemma, in mathcomp.ssreflect.finset]
-Def.aT [variable, in mathcomp.ssreflect.finfun]
-Def.n [variable, in mathcomp.ssreflect.tuple]
-Def.rT [variable, in mathcomp.ssreflect.finfun]
-Def.T [variable, in mathcomp.ssreflect.tuple]
-degree_irr1 [lemma, in mathcomp.character.mxrepresentation]
-degree_mxminpoly_map [lemma, in mathcomp.algebra.mxpoly]
-degree_mxminpoly [definition, in mathcomp.algebra.mxpoly]
-degree_mxminpoly_proof [lemma, in mathcomp.algebra.mxpoly]
-delta_mx_dshift [lemma, in mathcomp.algebra.matrix]
-delta_mx_ushift [lemma, in mathcomp.algebra.matrix]
-delta_mx_rshift [lemma, in mathcomp.algebra.matrix]
-delta_mx_lshift [lemma, in mathcomp.algebra.matrix]
-delta_mx [definition, in mathcomp.algebra.matrix]
-delta_mx_key [lemma, in mathcomp.algebra.matrix]
-denom_Ratio [lemma, in mathcomp.algebra.fraction]
-denom_ratioP [lemma, in mathcomp.algebra.fraction]
-denq [definition, in mathcomp.algebra.rat]
-denqN [lemma, in mathcomp.algebra.rat]
-denqP [lemma, in mathcomp.algebra.rat]
-denqVz [lemma, in mathcomp.algebra.rat]
-denq_norm [lemma, in mathcomp.algebra.rat]
-denq_mulr_sign [lemma, in mathcomp.algebra.rat]
-denq_int [lemma, in mathcomp.algebra.rat]
-denq_eq0 [lemma, in mathcomp.algebra.rat]
-denq_neq0 [lemma, in mathcomp.algebra.rat]
-denq_lt0 [lemma, in mathcomp.algebra.rat]
-denq_ge0 [definition, in mathcomp.algebra.rat]
-denq_gt0 [lemma, in mathcomp.algebra.rat]
-DepPlainTheory [section, in mathcomp.ssreflect.finfun]
-DepPlainTheory.aT [variable, in mathcomp.ssreflect.finfun]
-DepPlainTheory.F [variable, in mathcomp.ssreflect.finfun]
-DepPlainTheory.pT [variable, in mathcomp.ssreflect.finfun]
-DepPlainTheory.rT [variable, in mathcomp.ssreflect.finfun]
-Deprecation [module, in mathcomp.ssreflect.ssreflect]
-Deprecation.Exports [module, in mathcomp.ssreflect.ssreflect]
-Deprecation.Exports.deprecate [abbreviation, in mathcomp.ssreflect.ssreflect]
-Deprecation.exposed [definition, in mathcomp.ssreflect.ssreflect]
-Deprecation.hidden [definition, in mathcomp.ssreflect.ssreflect]
-Deprecation.hide [definition, in mathcomp.ssreflect.ssreflect]
-Deprecation.hint [projection, in mathcomp.ssreflect.ssreflect]
-Deprecation.Hint [constructor, in mathcomp.ssreflect.ssreflect]
-Deprecation.hinted [record, in mathcomp.ssreflect.ssreflect]
-Deprecation.Reject [module, in mathcomp.ssreflect.ssreflect]
-Deprecation.Reject [constructor, in mathcomp.ssreflect.ssreflect]
-Deprecation.reject [inductive, in mathcomp.ssreflect.ssreflect]
-Deprecation.reject_hint [definition, in mathcomp.ssreflect.ssreflect]
-Deprecation.Silent [module, in mathcomp.ssreflect.ssreflect]
-Deprecation.Silent [constructor, in mathcomp.ssreflect.ssreflect]
-Deprecation.silent [inductive, in mathcomp.ssreflect.ssreflect]
-Deprecation.silent_hint [definition, in mathcomp.ssreflect.ssreflect]
-Deprecation.statement [projection, in mathcomp.ssreflect.ssreflect]
-dergS [lemma, in mathcomp.solvable.commutator]
-dergSn [lemma, in mathcomp.solvable.commutator]
-derg0 [lemma, in mathcomp.solvable.commutator]
-derg1 [lemma, in mathcomp.solvable.commutator]
-derG1P [lemma, in mathcomp.solvable.commutator]
-deriv [definition, in mathcomp.algebra.poly]
-Derivation [definition, in mathcomp.field.separable]
-DerivationS [lemma, in mathcomp.field.separable]
-Derivation_separableP [lemma, in mathcomp.field.separable]
-Derivation_separable [lemma, in mathcomp.field.separable]
-Derivation_horner [lemma, in mathcomp.field.separable]
-Derivation_exp [lemma, in mathcomp.field.separable]
-Derivation_scalar [lemma, in mathcomp.field.separable]
-Derivation_mul_poly [lemma, in mathcomp.field.separable]
-Derivation_mul [lemma, in mathcomp.field.separable]
-Derivation1 [lemma, in mathcomp.field.separable]
-derivB [lemma, in mathcomp.algebra.poly]
-derivC [lemma, in mathcomp.algebra.poly]
-derivCE [definition, in mathcomp.algebra.poly]
-derivD [lemma, in mathcomp.algebra.poly]
-derivE [definition, in mathcomp.algebra.poly]
-DerivedBasics [section, in mathcomp.solvable.commutator]
-DerivedBasics.gT [variable, in mathcomp.solvable.commutator]
-DerivedGroup [section, in mathcomp.character.character]
-DerivedGroup.gT [variable, in mathcomp.character.character]
-derivedP [lemma, in mathcomp.solvable.nilpotent]
-derived_at [definition, in mathcomp.solvable.commutator]
-derived_at_rec [definition, in mathcomp.solvable.commutator]
-derivM [lemma, in mathcomp.algebra.poly]
-derivMn [lemma, in mathcomp.algebra.poly]
-derivMNn [lemma, in mathcomp.algebra.poly]
-derivMXaddC [lemma, in mathcomp.algebra.poly]
-derivMz [lemma, in mathcomp.algebra.ssrint]
-derivn [definition, in mathcomp.algebra.poly]
-derivN [lemma, in mathcomp.algebra.poly]
-derivnC [lemma, in mathcomp.algebra.poly]
-derivnD [lemma, in mathcomp.algebra.poly]
-derivnMn [lemma, in mathcomp.algebra.poly]
-derivnMNn [lemma, in mathcomp.algebra.poly]
-derivnMXaddC [lemma, in mathcomp.algebra.poly]
-derivnN [lemma, in mathcomp.algebra.poly]
-derivnS [lemma, in mathcomp.algebra.poly]
-derivnXn [lemma, in mathcomp.algebra.poly]
-derivnZ [lemma, in mathcomp.algebra.poly]
-derivn_map [lemma, in mathcomp.algebra.poly]
-derivn_poly0 [lemma, in mathcomp.algebra.poly]
-derivn_sub [lemma, in mathcomp.algebra.poly]
-derivn_is_linear [lemma, in mathcomp.algebra.poly]
-derivn0 [lemma, in mathcomp.algebra.poly]
-derivn1 [lemma, in mathcomp.algebra.poly]
-derivSn [lemma, in mathcomp.algebra.poly]
-derivX [lemma, in mathcomp.algebra.poly]
-derivXn [lemma, in mathcomp.algebra.poly]
-derivXsubC [lemma, in mathcomp.algebra.poly]
-derivZ [lemma, in mathcomp.algebra.poly]
-deriv_exp [lemma, in mathcomp.algebra.poly]
-deriv_comp [lemma, in mathcomp.algebra.poly]
-deriv_map [lemma, in mathcomp.algebra.poly]
-deriv_mulC [lemma, in mathcomp.algebra.poly]
-deriv_is_linear [lemma, in mathcomp.algebra.poly]
-deriv0 [lemma, in mathcomp.algebra.poly]
-derJ [lemma, in mathcomp.solvable.commutator]
-der_bigdprod [lemma, in mathcomp.solvable.nilpotent]
-der_bigcprod [lemma, in mathcomp.solvable.nilpotent]
-der_dprod [lemma, in mathcomp.solvable.nilpotent]
-der_cprod [lemma, in mathcomp.solvable.nilpotent]
-der_cont [lemma, in mathcomp.solvable.commutator]
-der_normalS [lemma, in mathcomp.solvable.commutator]
-der_subS [lemma, in mathcomp.solvable.commutator]
-der_normal [lemma, in mathcomp.solvable.commutator]
-der_norm [lemma, in mathcomp.solvable.commutator]
-der_sub [lemma, in mathcomp.solvable.commutator]
-der_char [lemma, in mathcomp.solvable.commutator]
-der_abelian [lemma, in mathcomp.solvable.commutator]
-der_group_set [lemma, in mathcomp.solvable.commutator]
-der1_sub_rker [lemma, in mathcomp.character.mxrepresentation]
-der1_stab_Ohm1_SCN_series [lemma, in mathcomp.solvable.maximal]
-der1_joing_cycles [lemma, in mathcomp.solvable.commutator]
-der1_min [lemma, in mathcomp.solvable.commutator]
-der1_subG [lemma, in mathcomp.fingroup.fingroup]
-determinant [definition, in mathcomp.algebra.matrix]
-determinant_alternate [lemma, in mathcomp.algebra.matrix]
-determinant_multilinear [lemma, in mathcomp.algebra.matrix]
-detM [lemma, in mathcomp.algebra.matrix]
-DetOrder [section, in mathcomp.character.character]
-DetOrder.DetRepr [section, in mathcomp.character.character]
-DetOrder.DetRepr.n [variable, in mathcomp.character.character]
-DetOrder.DetRepr.rG [variable, in mathcomp.character.character]
-DetOrder.G [variable, in mathcomp.character.character]
-DetOrder.gT [variable, in mathcomp.character.character]
-detRepr [definition, in mathcomp.character.character]
-detRepr_lin_char [lemma, in mathcomp.character.character]
-detV [lemma, in mathcomp.algebra.matrix]
-detZ [lemma, in mathcomp.algebra.matrix]
-det_inv [lemma, in mathcomp.algebra.matrix]
-det_lblock [lemma, in mathcomp.algebra.matrix]
-det_ublock [lemma, in mathcomp.algebra.matrix]
-det_diag [lemma, in mathcomp.algebra.matrix]
-det_mulmx [lemma, in mathcomp.algebra.matrix]
-det_scalar1 [lemma, in mathcomp.algebra.matrix]
-det_scalar [lemma, in mathcomp.algebra.matrix]
-det_mx00 [lemma, in mathcomp.algebra.matrix]
-det_perm [lemma, in mathcomp.algebra.matrix]
-det_tr [lemma, in mathcomp.algebra.matrix]
-det_map_mx [lemma, in mathcomp.algebra.matrix]
-det_is_repr [lemma, in mathcomp.character.character]
-det_repr_mx [definition, in mathcomp.character.character]
-det0 [lemma, in mathcomp.algebra.matrix]
-det0P [lemma, in mathcomp.algebra.matrix]
-det1 [lemma, in mathcomp.algebra.matrix]
-dffun_aT [abbreviation, in mathcomp.ssreflect.finfun]
-dfinfun_of [definition, in mathcomp.ssreflect.finfun]
-dfs [definition, in mathcomp.ssreflect.fingraph]
-dfsP [lemma, in mathcomp.ssreflect.fingraph]
-DfsPath [constructor, in mathcomp.ssreflect.fingraph]
-dfs_pathP [lemma, in mathcomp.ssreflect.fingraph]
-dfs_path [inductive, in mathcomp.ssreflect.fingraph]
-diag_mx_comm [lemma, in mathcomp.algebra.matrix]
-diag_mxC [lemma, in mathcomp.algebra.matrix]
-diag_const_mx [lemma, in mathcomp.algebra.matrix]
-diag_mx_sum_delta [lemma, in mathcomp.algebra.matrix]
-diag_mx_is_linear [lemma, in mathcomp.algebra.matrix]
-diag_mx [definition, in mathcomp.algebra.matrix]
-diag_mx_key [lemma, in mathcomp.algebra.matrix]
-diffmx [definition, in mathcomp.algebra.mxalgebra]
-diffmxE [lemma, in mathcomp.algebra.mxalgebra]
-diffmxSl [lemma, in mathcomp.algebra.mxalgebra]
-diffmx_key [lemma, in mathcomp.algebra.mxalgebra]
-diffmx_def [definition, in mathcomp.algebra.mxalgebra]
-diffv [definition, in mathcomp.algebra.vector]
-diffvSl [lemma, in mathcomp.algebra.vector]
-diffv_eq0 [lemma, in mathcomp.algebra.vector]
-diff_roots [definition, in mathcomp.algebra.poly]
-diff_id_sh [lemma, in mathcomp.solvable.burnside_app]
-Dihedral [constructor, in mathcomp.solvable.extremal]
-dihedral_classP [lemma, in mathcomp.solvable.extremal]
-dihedral_gtype [definition, in mathcomp.solvable.extremal]
-dihedral2_structure [lemma, in mathcomp.solvable.extremal]
-dIirr [definition, in mathcomp.character.vcharacter]
-dimv [definition, in mathcomp.algebra.vector]
-dimvf [lemma, in mathcomp.algebra.vector]
-dimvS [lemma, in mathcomp.algebra.vector]
-dimv_sum_leqif [lemma, in mathcomp.algebra.vector]
-dimv_leq_sum [lemma, in mathcomp.algebra.vector]
-dimv_add_leqif [lemma, in mathcomp.algebra.vector]
-dimv_disjoint_sum [lemma, in mathcomp.algebra.vector]
-dimv_sum_cap [lemma, in mathcomp.algebra.vector]
-dimv_cap_compl [lemma, in mathcomp.algebra.vector]
-dimv_compl [lemma, in mathcomp.algebra.vector]
-dimv_leqif_eq [lemma, in mathcomp.algebra.vector]
-dimv_leqif_sup [lemma, in mathcomp.algebra.vector]
-dimv_eq0 [lemma, in mathcomp.algebra.vector]
-dimv0 [lemma, in mathcomp.algebra.vector]
-dimv1 [lemma, in mathcomp.field.falgebra]
-dim_fixed_galois [lemma, in mathcomp.field.galois]
-dim_fixedField [lemma, in mathcomp.field.galois]
-dim_refBaseField [lemma, in mathcomp.field.fieldext]
-dim_baseVspace [lemma, in mathcomp.field.fieldext]
-dim_aspaceOver [lemma, in mathcomp.field.fieldext]
-dim_vspaceOver [lemma, in mathcomp.field.fieldext]
-dim_Fadjoin [lemma, in mathcomp.field.fieldext]
-dim_sup_field [lemma, in mathcomp.field.fieldext]
-dim_field_module [lemma, in mathcomp.field.fieldext]
-dim_cosetv [lemma, in mathcomp.field.fieldext]
-dim_span [lemma, in mathcomp.algebra.vector]
-dim_vline [lemma, in mathcomp.algebra.vector]
-dim_cfun_on_abelian [lemma, in mathcomp.character.classfun]
-dim_cfun_on [lemma, in mathcomp.character.classfun]
-dim_cfun [lemma, in mathcomp.character.classfun]
-dim_abelemE [lemma, in mathcomp.character.mxabelem]
-dim_cosetv_unit [lemma, in mathcomp.field.falgebra]
-dim_algid [lemma, in mathcomp.field.falgebra]
-dim_prodv [lemma, in mathcomp.field.falgebra]
-dinjectiveb [definition, in mathcomp.ssreflect.fintype]
-dinjectiveP [lemma, in mathcomp.ssreflect.fintype]
-dinjectivePn [lemma, in mathcomp.ssreflect.fintype]
-DirectSums [section, in mathcomp.algebra.mxalgebra]
-DirectSums.F [variable, in mathcomp.algebra.mxalgebra]
-DirectSums.I [variable, in mathcomp.algebra.mxalgebra]
-DirectSums.P [variable, in mathcomp.algebra.mxalgebra]
-directv [abbreviation, in mathcomp.algebra.vector]
-directv [abbreviation, in mathcomp.algebra.vector]
-directvE [lemma, in mathcomp.algebra.vector]
-directvEgeq [lemma, in mathcomp.algebra.vector]
-directvP [lemma, in mathcomp.algebra.vector]
-directv_sum_unique [lemma, in mathcomp.algebra.vector]
-directv_sum_independent [lemma, in mathcomp.algebra.vector]
-directv_sumE [lemma, in mathcomp.algebra.vector]
-directv_sumP [lemma, in mathcomp.algebra.vector]
-directv_add_unique [lemma, in mathcomp.algebra.vector]
-directv_addP [lemma, in mathcomp.algebra.vector]
-directv_addE [lemma, in mathcomp.algebra.vector]
-directv_trivial [lemma, in mathcomp.algebra.vector]
-directv_def [definition, in mathcomp.algebra.vector]
-direct_product [definition, in mathcomp.fingroup.gproduct]
-DirprodIsom [section, in mathcomp.fingroup.gproduct]
-DirprodIsom.gT [variable, in mathcomp.fingroup.gproduct]
-dirr [definition, in mathcomp.character.vcharacter]
-dirrE [lemma, in mathcomp.character.vcharacter]
-dIrrP [lemma, in mathcomp.character.vcharacter]
-dirrP [lemma, in mathcomp.character.vcharacter]
-dirr_small_norm [lemma, in mathcomp.character.vcharacter]
-dirr_constt_oppl [lemma, in mathcomp.character.vcharacter]
-dirr_constt_oppI [lemma, in mathcomp.character.vcharacter]
-dirr_constt_oppr [lemma, in mathcomp.character.vcharacter]
-dirr_consttE [lemma, in mathcomp.character.vcharacter]
-dirr_constt [definition, in mathcomp.character.vcharacter]
-dirr_dIirrE [lemma, in mathcomp.character.vcharacter]
-dirr_dIirrPE [lemma, in mathcomp.character.vcharacter]
-dirr_dIirr [definition, in mathcomp.character.vcharacter]
-dirr_inj [lemma, in mathcomp.character.vcharacter]
-dirr_dchi [lemma, in mathcomp.character.vcharacter]
-dirr_aut [lemma, in mathcomp.character.vcharacter]
-dirr_norm1 [lemma, in mathcomp.character.vcharacter]
-dirr_sign [lemma, in mathcomp.character.vcharacter]
-dirr_opp [lemma, in mathcomp.character.vcharacter]
-dirr_oppr_closed [lemma, in mathcomp.character.vcharacter]
-dirr_key [lemma, in mathcomp.character.vcharacter]
-dirr1 [definition, in mathcomp.character.vcharacter]
-dir_s0p [lemma, in mathcomp.solvable.burnside_app]
-dir_iso_iso3 [lemma, in mathcomp.solvable.burnside_app]
-dir_iso3l [definition, in mathcomp.solvable.burnside_app]
-dir_iso3 [definition, in mathcomp.solvable.burnside_app]
-disjoint [definition, in mathcomp.ssreflect.fintype]
-disjoints_subset [lemma, in mathcomp.ssreflect.finset]
-disjointU [lemma, in mathcomp.ssreflect.fintype]
-disjointU1 [lemma, in mathcomp.ssreflect.fintype]
-disjoint_cat [lemma, in mathcomp.ssreflect.fintype]
-disjoint_has [lemma, in mathcomp.ssreflect.fintype]
-disjoint_cons [lemma, in mathcomp.ssreflect.fintype]
-disjoint_trans [lemma, in mathcomp.ssreflect.fintype]
-disjoint_subset [lemma, in mathcomp.ssreflect.fintype]
-disjoint_sym [lemma, in mathcomp.ssreflect.fintype]
-disjoint_setI0 [lemma, in mathcomp.ssreflect.finset]
-disjoint0 [lemma, in mathcomp.ssreflect.fintype]
-disjoint1 [lemma, in mathcomp.ssreflect.fintype]
-Distributivity [section, in mathcomp.ssreflect.bigop]
-Distributivity.one [variable, in mathcomp.ssreflect.bigop]
-Distributivity.plus [variable, in mathcomp.ssreflect.bigop]
-Distributivity.R [variable, in mathcomp.ssreflect.bigop]
-Distributivity.times [variable, in mathcomp.ssreflect.bigop]
-Distributivity.zero [variable, in mathcomp.ssreflect.bigop]
-_ + _ [notation, in mathcomp.ssreflect.bigop]
-_ * _ [notation, in mathcomp.ssreflect.bigop]
-*%M [notation, in mathcomp.ssreflect.bigop]
-+%M [notation, in mathcomp.ssreflect.bigop]
-0 [notation, in mathcomp.ssreflect.bigop]
-1 [notation, in mathcomp.ssreflect.bigop]
-div [library]
-divgI [lemma, in mathcomp.fingroup.fingroup]
-divgr [definition, in mathcomp.fingroup.gproduct]
-divgrM [lemma, in mathcomp.fingroup.gproduct]
-divgrMid [lemma, in mathcomp.fingroup.gproduct]
-divgrMl [lemma, in mathcomp.fingroup.gproduct]
-divgr_id [lemma, in mathcomp.fingroup.gproduct]
-divgr_eq [lemma, in mathcomp.fingroup.gproduct]
-divgS [lemma, in mathcomp.fingroup.fingroup]
-divg_normal [lemma, in mathcomp.fingroup.quotient]
-divg_indexS [lemma, in mathcomp.fingroup.fingroup]
-divg_index [lemma, in mathcomp.fingroup.fingroup]
-divisors [definition, in mathcomp.ssreflect.prime]
-divisors_id [lemma, in mathcomp.ssreflect.prime]
-divisors_uniq [lemma, in mathcomp.ssreflect.prime]
-divisors_correct [lemma, in mathcomp.ssreflect.prime]
-divisor1 [lemma, in mathcomp.ssreflect.prime]
-divn [definition, in mathcomp.ssreflect.div]
-divnA [lemma, in mathcomp.ssreflect.div]
-divnAC [lemma, in mathcomp.ssreflect.div]
-divnDl [lemma, in mathcomp.ssreflect.div]
-divnDr [lemma, in mathcomp.ssreflect.div]
-divnK [lemma, in mathcomp.ssreflect.div]
-divnMA [lemma, in mathcomp.ssreflect.div]
-divnMDl [lemma, in mathcomp.ssreflect.div]
-divnMl [lemma, in mathcomp.ssreflect.div]
-divnMr [lemma, in mathcomp.ssreflect.div]
-divnn [lemma, in mathcomp.ssreflect.div]
-divNz_nat [lemma, in mathcomp.algebra.intdiv]
-divn_count_dvd [lemma, in mathcomp.ssreflect.prime]
-divn_mulAC [lemma, in mathcomp.ssreflect.div]
-divn_gt0 [lemma, in mathcomp.ssreflect.div]
-divn_small [lemma, in mathcomp.ssreflect.div]
-divn_eq [lemma, in mathcomp.ssreflect.div]
-divn0 [lemma, in mathcomp.ssreflect.div]
-divn1 [lemma, in mathcomp.ssreflect.div]
-divn2 [lemma, in mathcomp.ssreflect.div]
-divp_polyOver [lemma, in mathcomp.field.fieldext]
-divq [definition, in mathcomp.algebra.rat]
-divqP [lemma, in mathcomp.algebra.rat]
-DivqSpecN [constructor, in mathcomp.algebra.rat]
-DivqSpecP [constructor, in mathcomp.algebra.rat]
-divq_eq [lemma, in mathcomp.algebra.rat]
-divq_spec [inductive, in mathcomp.algebra.rat]
-divq_num_den [lemma, in mathcomp.algebra.rat]
-divz [definition, in mathcomp.algebra.intdiv]
-divzA [lemma, in mathcomp.algebra.intdiv]
-divzAC [lemma, in mathcomp.algebra.intdiv]
-divzDl [lemma, in mathcomp.algebra.intdiv]
-divzDr [lemma, in mathcomp.algebra.intdiv]
-divzK [lemma, in mathcomp.algebra.intdiv]
-divzMA [lemma, in mathcomp.algebra.intdiv]
-divzMA_ge0 [lemma, in mathcomp.algebra.intdiv]
-divzMDl [lemma, in mathcomp.algebra.intdiv]
-divzMl [lemma, in mathcomp.algebra.intdiv]
-divzMpl [lemma, in mathcomp.algebra.intdiv]
-divzMpr [lemma, in mathcomp.algebra.intdiv]
-divzMr [lemma, in mathcomp.algebra.intdiv]
-divzN [lemma, in mathcomp.algebra.intdiv]
-divzz [lemma, in mathcomp.algebra.intdiv]
-divz_mulAC [lemma, in mathcomp.algebra.intdiv]
-divz_ge0 [lemma, in mathcomp.algebra.intdiv]
-divz_small [lemma, in mathcomp.algebra.intdiv]
-divz_eq [lemma, in mathcomp.algebra.intdiv]
-divz_abs [lemma, in mathcomp.algebra.intdiv]
-divz_nat [lemma, in mathcomp.algebra.intdiv]
-divz0 [lemma, in mathcomp.algebra.intdiv]
-divz1 [lemma, in mathcomp.algebra.intdiv]
-div_annihilantP [lemma, in mathcomp.algebra.polyXY]
-div_annihilant_neq0 [lemma, in mathcomp.algebra.polyXY]
-div_annihilant_in_ideal [lemma, in mathcomp.algebra.polyXY]
-div_annihilant [definition, in mathcomp.algebra.polyXY]
-div_ring_mul_group_cyclic [lemma, in mathcomp.solvable.cyclic]
-div0n [lemma, in mathcomp.ssreflect.div]
-div0z [lemma, in mathcomp.algebra.intdiv]
-dlsubmx [definition, in mathcomp.algebra.matrix]
-DnQ_extraspecial [lemma, in mathcomp.solvable.extraspecial]
-DnQ_pgroup [lemma, in mathcomp.solvable.extraspecial]
-DnQ_P [lemma, in mathcomp.solvable.extraspecial]
-dom [abbreviation, in mathcomp.fingroup.action]
-dom [definition, in mathcomp.fingroup.morphism]
-domP [lemma, in mathcomp.fingroup.morphism]
-dom_hom_mx_module [lemma, in mathcomp.character.mxrepresentation]
-dom_hom_invmx [lemma, in mathcomp.character.mxrepresentation]
-dom_hom_mx [definition, in mathcomp.character.mxrepresentation]
-dom_qactJ [lemma, in mathcomp.fingroup.action]
-dom_ker [lemma, in mathcomp.fingroup.morphism]
-DotProduct [section, in mathcomp.character.classfun]
-DotProduct.G [variable, in mathcomp.character.classfun]
-DotProduct.gT [variable, in mathcomp.character.classfun]
-double [definition, in mathcomp.ssreflect.ssrnat]
-doubleB [lemma, in mathcomp.ssreflect.ssrnat]
-doubleD [lemma, in mathcomp.ssreflect.ssrnat]
-doubleE [lemma, in mathcomp.ssreflect.ssrnat]
-doubleK [lemma, in mathcomp.ssreflect.ssrnat]
-doubleMl [lemma, in mathcomp.ssreflect.ssrnat]
-doubleMr [lemma, in mathcomp.ssreflect.ssrnat]
-doubleS [lemma, in mathcomp.ssreflect.ssrnat]
-double_inj [definition, in mathcomp.ssreflect.ssrnat]
-double_eq0 [lemma, in mathcomp.ssreflect.ssrnat]
-double_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
-double_rec [definition, in mathcomp.ssreflect.ssrnat]
-double0 [lemma, in mathcomp.ssreflect.ssrnat]
-dpair [definition, in mathcomp.fingroup.perm]
-dprod [abbreviation, in mathcomp.fingroup.gproduct]
-dprod [abbreviation, in mathcomp.fingroup.gproduct]
-DProd [section, in mathcomp.character.character]
-dprodA [lemma, in mathcomp.fingroup.gproduct]
-dprodC [lemma, in mathcomp.fingroup.gproduct]
-dprodE [lemma, in mathcomp.fingroup.gproduct]
-dprodEcp [lemma, in mathcomp.fingroup.gproduct]
-dprodEsd [lemma, in mathcomp.fingroup.gproduct]
-dprodEY [lemma, in mathcomp.fingroup.gproduct]
-dprodg1 [lemma, in mathcomp.fingroup.gproduct]
-dprodJ [lemma, in mathcomp.fingroup.gproduct]
-dprodl_Iirr0 [lemma, in mathcomp.character.character]
-dprodl_Iirr_eq0 [lemma, in mathcomp.character.character]
-dprodl_IirrK [lemma, in mathcomp.character.character]
-dprodl_IirrE [lemma, in mathcomp.character.character]
-dprodl_Iirr [definition, in mathcomp.character.character]
-dprodm [definition, in mathcomp.fingroup.gproduct]
-dprodmE [lemma, in mathcomp.fingroup.gproduct]
-dprodmEl [lemma, in mathcomp.fingroup.gproduct]
-dprodmEr [lemma, in mathcomp.fingroup.gproduct]
-dprodm_eqf [lemma, in mathcomp.fingroup.gproduct]
-dprodm_cprod [lemma, in mathcomp.fingroup.gproduct]
-dprodP [lemma, in mathcomp.fingroup.gproduct]
-dprodr_Iirr0 [lemma, in mathcomp.character.character]
-dprodr_Iirr_eq0 [lemma, in mathcomp.character.character]
-dprodr_IirrK [lemma, in mathcomp.character.character]
-dprodr_IirrE [lemma, in mathcomp.character.character]
-dprodr_Iirr [definition, in mathcomp.character.character]
-DProduct [section, in mathcomp.character.classfun]
-DProduct.cKH [variable, in mathcomp.character.classfun]
-DProduct.G [variable, in mathcomp.character.classfun]
-DProduct.gT [variable, in mathcomp.character.classfun]
-DProduct.H [variable, in mathcomp.character.classfun]
-DProduct.K [variable, in mathcomp.character.classfun]
-DProduct.KxH [variable, in mathcomp.character.classfun]
-DProduct.nsHG [variable, in mathcomp.character.classfun]
-DProduct.nsKG [variable, in mathcomp.character.classfun]
-DProduct.sHG [variable, in mathcomp.character.classfun]
-DProduct.sKG [variable, in mathcomp.character.classfun]
-dprodW [lemma, in mathcomp.fingroup.gproduct]
-dprodWC [lemma, in mathcomp.fingroup.gproduct]
-dprodWcp [lemma, in mathcomp.fingroup.gproduct]
-dprodWsd [lemma, in mathcomp.fingroup.gproduct]
-dprodWsdC [lemma, in mathcomp.fingroup.gproduct]
-dprodWY [lemma, in mathcomp.fingroup.gproduct]
-dprodYP [lemma, in mathcomp.fingroup.gproduct]
-dprod_card [lemma, in mathcomp.fingroup.gproduct]
-dprod_modr [lemma, in mathcomp.fingroup.gproduct]
-dprod_modl [lemma, in mathcomp.fingroup.gproduct]
-dprod_normal2 [lemma, in mathcomp.fingroup.gproduct]
-dprod_IirrC [lemma, in mathcomp.character.character]
-dprod_IirrK [lemma, in mathcomp.character.character]
-dprod_Iirr_onto [lemma, in mathcomp.character.character]
-dprod_Iirr_eq0 [lemma, in mathcomp.character.character]
-dprod_Iirr0r [lemma, in mathcomp.character.character]
-dprod_Iirr0l [lemma, in mathcomp.character.character]
-dprod_Iirr0 [lemma, in mathcomp.character.character]
-dprod_Iirr_inj [lemma, in mathcomp.character.character]
-dprod_IirrEr [lemma, in mathcomp.character.character]
-dprod_IirrEl [lemma, in mathcomp.character.character]
-dprod_IirrE [lemma, in mathcomp.character.character]
-dprod_Iirr [definition, in mathcomp.character.character]
-dprod_homocyclic [lemma, in mathcomp.solvable.abelian]
-dprod_abelem [lemma, in mathcomp.solvable.abelian]
-dprod_exponent [lemma, in mathcomp.solvable.abelian]
-dprod_rowg [lemma, in mathcomp.character.mxabelem]
-dprod_nil [lemma, in mathcomp.solvable.nilpotent]
-DProd.G [variable, in mathcomp.character.character]
-DProd.gT [variable, in mathcomp.character.character]
-DProd.H [variable, in mathcomp.character.character]
-DProd.K [variable, in mathcomp.character.character]
-DProd.KxH [variable, in mathcomp.character.character]
-dprod1g [lemma, in mathcomp.fingroup.gproduct]
-drop [definition, in mathcomp.ssreflect.seq]
-drop_tupleP [lemma, in mathcomp.ssreflect.tuple]
-drop_subseq [lemma, in mathcomp.ssreflect.seq]
-drop_rev [lemma, in mathcomp.ssreflect.seq]
-drop_nth [lemma, in mathcomp.ssreflect.seq]
-drop_rcons [lemma, in mathcomp.ssreflect.seq]
-drop_drop [lemma, in mathcomp.ssreflect.seq]
-drop_size_cat [lemma, in mathcomp.ssreflect.seq]
-drop_cat [lemma, in mathcomp.ssreflect.seq]
-drop_cons [lemma, in mathcomp.ssreflect.seq]
-drop_size [lemma, in mathcomp.ssreflect.seq]
-drop_oversize [lemma, in mathcomp.ssreflect.seq]
-drop_behead [lemma, in mathcomp.ssreflect.seq]
-drop0 [lemma, in mathcomp.ssreflect.seq]
-drop1 [lemma, in mathcomp.ssreflect.seq]
-drsubmx [definition, in mathcomp.algebra.matrix]
-dsubmx [definition, in mathcomp.algebra.matrix]
-dsubmx_key [lemma, in mathcomp.algebra.matrix]
-dsumx_mul [lemma, in mathcomp.character.character]
-dtuple_on_subset [lemma, in mathcomp.solvable.primitive_action]
-dtuple_on_add_D1 [lemma, in mathcomp.solvable.primitive_action]
-dtuple_on_add [lemma, in mathcomp.solvable.primitive_action]
-dtuple_onP [lemma, in mathcomp.solvable.primitive_action]
-dtuple_on [definition, in mathcomp.solvable.primitive_action]
-dvdA [definition, in mathcomp.field.algnum]
-dvdA_zmod_closed [lemma, in mathcomp.field.algnum]
-dvdA_key [lemma, in mathcomp.field.algnum]
-dvdCP [lemma, in mathcomp.field.algC]
-dvdCP_nat [lemma, in mathcomp.field.algC]
-dvdC_int [lemma, in mathcomp.field.algC]
-dvdC_nat [lemma, in mathcomp.field.algC]
-dvdC_zmod [lemma, in mathcomp.field.algC]
-dvdC_key [lemma, in mathcomp.field.algC]
-dvdC_refl [lemma, in mathcomp.field.algC]
-dvdC_trans [lemma, in mathcomp.field.algC]
-dvdC_mul2l [lemma, in mathcomp.field.algC]
-dvdC_mul2r [lemma, in mathcomp.field.algC]
-dvdC_mulr [lemma, in mathcomp.field.algC]
-dvdC_mull [lemma, in mathcomp.field.algC]
-dvdC0 [lemma, in mathcomp.field.algC]
-dvdn [definition, in mathcomp.ssreflect.div]
-dvdnn [lemma, in mathcomp.ssreflect.div]
-dvdnP [lemma, in mathcomp.ssreflect.div]
-dvdn_quotient [lemma, in mathcomp.fingroup.quotient]
-dvdn_morphim [lemma, in mathcomp.fingroup.quotient]
-dvdn_pred_predX [lemma, in mathcomp.ssreflect.binomial]
-dvdn_partP [lemma, in mathcomp.ssreflect.prime]
-dvdn_sum [lemma, in mathcomp.ssreflect.prime]
-dvdn_divisors [lemma, in mathcomp.ssreflect.prime]
-dvdn_part [lemma, in mathcomp.ssreflect.prime]
-dvdn_pfactor [lemma, in mathcomp.ssreflect.prime]
-dvdn_leq_log [lemma, in mathcomp.ssreflect.prime]
-dvdn_prime2 [lemma, in mathcomp.ssreflect.prime]
-dvdn_pexp2r [lemma, in mathcomp.ssreflect.div]
-dvdn_double_ltn [lemma, in mathcomp.ssreflect.div]
-dvdn_double_leq [lemma, in mathcomp.ssreflect.div]
-dvdn_lcm [lemma, in mathcomp.ssreflect.div]
-dvdn_lcmr [lemma, in mathcomp.ssreflect.div]
-dvdn_lcml [lemma, in mathcomp.ssreflect.div]
-dvdn_gcd [lemma, in mathcomp.ssreflect.div]
-dvdn_gcdl [lemma, in mathcomp.ssreflect.div]
-dvdn_gcdr [lemma, in mathcomp.ssreflect.div]
-dvdn_fact [lemma, in mathcomp.ssreflect.div]
-dvdn_exp [lemma, in mathcomp.ssreflect.div]
-dvdn_sub [lemma, in mathcomp.ssreflect.div]
-dvdn_subl [lemma, in mathcomp.ssreflect.div]
-dvdn_subr [lemma, in mathcomp.ssreflect.div]
-dvdn_add_eq [lemma, in mathcomp.ssreflect.div]
-dvdn_add [lemma, in mathcomp.ssreflect.div]
-dvdn_addl [lemma, in mathcomp.ssreflect.div]
-dvdn_addr [lemma, in mathcomp.ssreflect.div]
-dvdn_exp2r [lemma, in mathcomp.ssreflect.div]
-dvdn_Pexp2l [lemma, in mathcomp.ssreflect.div]
-dvdn_exp2l [lemma, in mathcomp.ssreflect.div]
-dvdn_div [lemma, in mathcomp.ssreflect.div]
-dvdn_divRL [lemma, in mathcomp.ssreflect.div]
-dvdn_divLR [lemma, in mathcomp.ssreflect.div]
-dvdn_pmul2r [lemma, in mathcomp.ssreflect.div]
-dvdn_pmul2l [lemma, in mathcomp.ssreflect.div]
-dvdn_leq [lemma, in mathcomp.ssreflect.div]
-dvdn_odd [lemma, in mathcomp.ssreflect.div]
-dvdn_eq [lemma, in mathcomp.ssreflect.div]
-dvdn_trans [lemma, in mathcomp.ssreflect.div]
-dvdn_mul [lemma, in mathcomp.ssreflect.div]
-dvdn_mulr [lemma, in mathcomp.ssreflect.div]
-dvdn_mull [lemma, in mathcomp.ssreflect.div]
-dvdn_gt0 [lemma, in mathcomp.ssreflect.div]
-dvdn_orderC [lemma, in mathcomp.field.algnum]
-dvdn_constt_Res1_irr1 [lemma, in mathcomp.character.inertia]
-dvdn_exponent [lemma, in mathcomp.solvable.abelian]
-dvdn_orbit [lemma, in mathcomp.fingroup.action]
-dvdn_cforder [lemma, in mathcomp.character.classfun]
-dvdn_cforderP [lemma, in mathcomp.character.classfun]
-dvdn_prim_root [lemma, in mathcomp.algebra.poly]
-dvdn_biggcdP [lemma, in mathcomp.ssreflect.bigop]
-dvdn_biglcmP [lemma, in mathcomp.ssreflect.bigop]
-dvdn_cardMg [lemma, in mathcomp.fingroup.fingroup]
-dvdn_indexg [lemma, in mathcomp.fingroup.fingroup]
-dvdn_prime_cyclic [lemma, in mathcomp.solvable.cyclic]
-dvdn0 [lemma, in mathcomp.ssreflect.div]
-dvdn1 [lemma, in mathcomp.ssreflect.div]
-dvdn2 [lemma, in mathcomp.ssreflect.div]
-dvdpP_rat_int [lemma, in mathcomp.algebra.intdiv]
-dvdpP_int [lemma, in mathcomp.algebra.intdiv]
-dvdp_separable [lemma, in mathcomp.field.separable]
-dvdp_rat_int [lemma, in mathcomp.algebra.intdiv]
-dvdz [definition, in mathcomp.algebra.intdiv]
-dvdzE [lemma, in mathcomp.algebra.intdiv]
-dvdzP [lemma, in mathcomp.algebra.intdiv]
-dvdzz [lemma, in mathcomp.algebra.intdiv]
-dvdz_contents [lemma, in mathcomp.algebra.intdiv]
-dvdz_pexp2r [lemma, in mathcomp.algebra.intdiv]
-dvdz_gcd [lemma, in mathcomp.algebra.intdiv]
-dvdz_gcdl [lemma, in mathcomp.algebra.intdiv]
-dvdz_gcdr [lemma, in mathcomp.algebra.intdiv]
-dvdz_exp [lemma, in mathcomp.algebra.intdiv]
-dvdz_zmod_closed [lemma, in mathcomp.algebra.intdiv]
-dvdz_exp2r [lemma, in mathcomp.algebra.intdiv]
-dvdz_Pexp2l [lemma, in mathcomp.algebra.intdiv]
-dvdz_exp2l [lemma, in mathcomp.algebra.intdiv]
-dvdz_mul2r [lemma, in mathcomp.algebra.intdiv]
-dvdz_mul2l [lemma, in mathcomp.algebra.intdiv]
-dvdz_eq [lemma, in mathcomp.algebra.intdiv]
-dvdz_mod0P [lemma, in mathcomp.algebra.intdiv]
-dvdz_trans [lemma, in mathcomp.algebra.intdiv]
-dvdz_mul [lemma, in mathcomp.algebra.intdiv]
-dvdz_mulr [lemma, in mathcomp.algebra.intdiv]
-dvdz_mull [lemma, in mathcomp.algebra.intdiv]
-dvdz_key [lemma, in mathcomp.algebra.intdiv]
-dvdz0 [lemma, in mathcomp.algebra.intdiv]
-dvdz1 [lemma, in mathcomp.algebra.intdiv]
-dvd_irr1_index_center [lemma, in mathcomp.character.integral_char]
-dvd_irr1_cardG [lemma, in mathcomp.character.integral_char]
-dvd0C [lemma, in mathcomp.field.algC]
-dvd0n [lemma, in mathcomp.ssreflect.div]
-dvd0z [lemma, in mathcomp.algebra.intdiv]
-dvd1n [lemma, in mathcomp.ssreflect.div]
-dvd1z [lemma, in mathcomp.algebra.intdiv]
-
| Global Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(23836 entries) | -
| Notation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1409 entries) | -
| Module Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(221 entries) | -
| Variable Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3574 entries) | -
| Library Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(90 entries) | -
| Lemma Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(12096 entries) | -
| Constructor Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(368 entries) | -
| Axiom Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(45 entries) | -
| Inductive Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(107 entries) | -
| Projection Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(273 entries) | -
| Section Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1140 entries) | -
| Abbreviation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(728 entries) | -
| Definition Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3596 entries) | -
| Record Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(189 entries) | -