| 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 (lemma)
-daddv_pi_add [in mathcomp.algebra.vector]-daddv_pi_proj [in mathcomp.algebra.vector]
-daddv_pi_id [in mathcomp.algebra.vector]
-dchi_vchar [in mathcomp.character.vcharacter]
-dchi_ndirrE [in mathcomp.character.vcharacter]
-dchi1 [in mathcomp.character.vcharacter]
-decrn_inj_in [in mathcomp.ssreflect.ssrnat]
-decrn_inj [in mathcomp.ssreflect.ssrnat]
-DecSocleType [in mathcomp.character.mxrepresentation]
-dec_mx_reducible_semisimple [in mathcomp.character.mxrepresentation]
-dec_mxsimple_exists [in mathcomp.character.mxrepresentation]
-dec_Qint_span [in mathcomp.algebra.intdiv]
-dec_Cint_span [in mathcomp.field.algnum]
-dec_factor_theorem [in mathcomp.algebra.poly]
-def_pnElem [in mathcomp.solvable.abelian]
-def_pblock [in mathcomp.ssreflect.finset]
-degree_irr1 [in mathcomp.character.mxrepresentation]
-degree_mxminpoly_map [in mathcomp.algebra.mxpoly]
-degree_mxminpoly_proof [in mathcomp.algebra.mxpoly]
-delta_mx_dshift [in mathcomp.algebra.matrix]
-delta_mx_ushift [in mathcomp.algebra.matrix]
-delta_mx_rshift [in mathcomp.algebra.matrix]
-delta_mx_lshift [in mathcomp.algebra.matrix]
-delta_mx_key [in mathcomp.algebra.matrix]
-denom_Ratio [in mathcomp.algebra.fraction]
-denom_ratioP [in mathcomp.algebra.fraction]
-denqN [in mathcomp.algebra.rat]
-denqP [in mathcomp.algebra.rat]
-denqVz [in mathcomp.algebra.rat]
-denq_norm [in mathcomp.algebra.rat]
-denq_mulr_sign [in mathcomp.algebra.rat]
-denq_int [in mathcomp.algebra.rat]
-denq_eq0 [in mathcomp.algebra.rat]
-denq_neq0 [in mathcomp.algebra.rat]
-denq_lt0 [in mathcomp.algebra.rat]
-denq_gt0 [in mathcomp.algebra.rat]
-dergS [in mathcomp.solvable.commutator]
-dergSn [in mathcomp.solvable.commutator]
-derg0 [in mathcomp.solvable.commutator]
-derg1 [in mathcomp.solvable.commutator]
-derG1P [in mathcomp.solvable.commutator]
-DerivationS [in mathcomp.field.separable]
-Derivation_separableP [in mathcomp.field.separable]
-Derivation_separable [in mathcomp.field.separable]
-Derivation_horner [in mathcomp.field.separable]
-Derivation_exp [in mathcomp.field.separable]
-Derivation_scalar [in mathcomp.field.separable]
-Derivation_mul_poly [in mathcomp.field.separable]
-Derivation_mul [in mathcomp.field.separable]
-Derivation1 [in mathcomp.field.separable]
-derivB [in mathcomp.algebra.poly]
-derivC [in mathcomp.algebra.poly]
-derivD [in mathcomp.algebra.poly]
-derivedP [in mathcomp.solvable.nilpotent]
-derivM [in mathcomp.algebra.poly]
-derivMn [in mathcomp.algebra.poly]
-derivMNn [in mathcomp.algebra.poly]
-derivMXaddC [in mathcomp.algebra.poly]
-derivMz [in mathcomp.algebra.ssrint]
-derivN [in mathcomp.algebra.poly]
-derivnC [in mathcomp.algebra.poly]
-derivnD [in mathcomp.algebra.poly]
-derivnMn [in mathcomp.algebra.poly]
-derivnMNn [in mathcomp.algebra.poly]
-derivnMXaddC [in mathcomp.algebra.poly]
-derivnN [in mathcomp.algebra.poly]
-derivnS [in mathcomp.algebra.poly]
-derivnXn [in mathcomp.algebra.poly]
-derivnZ [in mathcomp.algebra.poly]
-derivn_map [in mathcomp.algebra.poly]
-derivn_poly0 [in mathcomp.algebra.poly]
-derivn_sub [in mathcomp.algebra.poly]
-derivn_is_linear [in mathcomp.algebra.poly]
-derivn0 [in mathcomp.algebra.poly]
-derivn1 [in mathcomp.algebra.poly]
-derivSn [in mathcomp.algebra.poly]
-derivX [in mathcomp.algebra.poly]
-derivXn [in mathcomp.algebra.poly]
-derivXsubC [in mathcomp.algebra.poly]
-derivZ [in mathcomp.algebra.poly]
-deriv_exp [in mathcomp.algebra.poly]
-deriv_comp [in mathcomp.algebra.poly]
-deriv_map [in mathcomp.algebra.poly]
-deriv_mulC [in mathcomp.algebra.poly]
-deriv_is_linear [in mathcomp.algebra.poly]
-deriv0 [in mathcomp.algebra.poly]
-derJ [in mathcomp.solvable.commutator]
-der_bigdprod [in mathcomp.solvable.nilpotent]
-der_bigcprod [in mathcomp.solvable.nilpotent]
-der_dprod [in mathcomp.solvable.nilpotent]
-der_cprod [in mathcomp.solvable.nilpotent]
-der_cont [in mathcomp.solvable.commutator]
-der_normalS [in mathcomp.solvable.commutator]
-der_subS [in mathcomp.solvable.commutator]
-der_normal [in mathcomp.solvable.commutator]
-der_norm [in mathcomp.solvable.commutator]
-der_sub [in mathcomp.solvable.commutator]
-der_char [in mathcomp.solvable.commutator]
-der_abelian [in mathcomp.solvable.commutator]
-der_group_set [in mathcomp.solvable.commutator]
-der1_sub_rker [in mathcomp.character.mxrepresentation]
-der1_stab_Ohm1_SCN_series [in mathcomp.solvable.maximal]
-der1_joing_cycles [in mathcomp.solvable.commutator]
-der1_min [in mathcomp.solvable.commutator]
-der1_subG [in mathcomp.fingroup.fingroup]
-determinant_alternate [in mathcomp.algebra.matrix]
-determinant_multilinear [in mathcomp.algebra.matrix]
-detM [in mathcomp.algebra.matrix]
-detRepr_lin_char [in mathcomp.character.character]
-detV [in mathcomp.algebra.matrix]
-detZ [in mathcomp.algebra.matrix]
-det_inv [in mathcomp.algebra.matrix]
-det_lblock [in mathcomp.algebra.matrix]
-det_ublock [in mathcomp.algebra.matrix]
-det_diag [in mathcomp.algebra.matrix]
-det_mulmx [in mathcomp.algebra.matrix]
-det_scalar1 [in mathcomp.algebra.matrix]
-det_scalar [in mathcomp.algebra.matrix]
-det_mx00 [in mathcomp.algebra.matrix]
-det_perm [in mathcomp.algebra.matrix]
-det_tr [in mathcomp.algebra.matrix]
-det_map_mx [in mathcomp.algebra.matrix]
-det_is_repr [in mathcomp.character.character]
-det0 [in mathcomp.algebra.matrix]
-det0P [in mathcomp.algebra.matrix]
-det1 [in mathcomp.algebra.matrix]
-dfsP [in mathcomp.ssreflect.fingraph]
-dfs_pathP [in mathcomp.ssreflect.fingraph]
-diag_mx_comm [in mathcomp.algebra.matrix]
-diag_mxC [in mathcomp.algebra.matrix]
-diag_const_mx [in mathcomp.algebra.matrix]
-diag_mx_sum_delta [in mathcomp.algebra.matrix]
-diag_mx_is_linear [in mathcomp.algebra.matrix]
-diag_mx_key [in mathcomp.algebra.matrix]
-diffmxE [in mathcomp.algebra.mxalgebra]
-diffmxSl [in mathcomp.algebra.mxalgebra]
-diffmx_key [in mathcomp.algebra.mxalgebra]
-diffvSl [in mathcomp.algebra.vector]
-diffv_eq0 [in mathcomp.algebra.vector]
-diff_id_sh [in mathcomp.solvable.burnside_app]
-dihedral_classP [in mathcomp.solvable.extremal]
-dihedral2_structure [in mathcomp.solvable.extremal]
-dimvf [in mathcomp.algebra.vector]
-dimvS [in mathcomp.algebra.vector]
-dimv_sum_leqif [in mathcomp.algebra.vector]
-dimv_leq_sum [in mathcomp.algebra.vector]
-dimv_add_leqif [in mathcomp.algebra.vector]
-dimv_disjoint_sum [in mathcomp.algebra.vector]
-dimv_sum_cap [in mathcomp.algebra.vector]
-dimv_cap_compl [in mathcomp.algebra.vector]
-dimv_compl [in mathcomp.algebra.vector]
-dimv_leqif_eq [in mathcomp.algebra.vector]
-dimv_leqif_sup [in mathcomp.algebra.vector]
-dimv_eq0 [in mathcomp.algebra.vector]
-dimv0 [in mathcomp.algebra.vector]
-dimv1 [in mathcomp.field.falgebra]
-dim_fixed_galois [in mathcomp.field.galois]
-dim_fixedField [in mathcomp.field.galois]
-dim_refBaseField [in mathcomp.field.fieldext]
-dim_baseVspace [in mathcomp.field.fieldext]
-dim_aspaceOver [in mathcomp.field.fieldext]
-dim_vspaceOver [in mathcomp.field.fieldext]
-dim_Fadjoin [in mathcomp.field.fieldext]
-dim_sup_field [in mathcomp.field.fieldext]
-dim_field_module [in mathcomp.field.fieldext]
-dim_cosetv [in mathcomp.field.fieldext]
-dim_span [in mathcomp.algebra.vector]
-dim_vline [in mathcomp.algebra.vector]
-dim_cfun_on_abelian [in mathcomp.character.classfun]
-dim_cfun_on [in mathcomp.character.classfun]
-dim_cfun [in mathcomp.character.classfun]
-dim_abelemE [in mathcomp.character.mxabelem]
-dim_cosetv_unit [in mathcomp.field.falgebra]
-dim_algid [in mathcomp.field.falgebra]
-dim_prodv [in mathcomp.field.falgebra]
-dinjectiveP [in mathcomp.ssreflect.fintype]
-dinjectivePn [in mathcomp.ssreflect.fintype]
-directvE [in mathcomp.algebra.vector]
-directvEgeq [in mathcomp.algebra.vector]
-directvP [in mathcomp.algebra.vector]
-directv_sum_unique [in mathcomp.algebra.vector]
-directv_sum_independent [in mathcomp.algebra.vector]
-directv_sumE [in mathcomp.algebra.vector]
-directv_sumP [in mathcomp.algebra.vector]
-directv_add_unique [in mathcomp.algebra.vector]
-directv_addP [in mathcomp.algebra.vector]
-directv_addE [in mathcomp.algebra.vector]
-directv_trivial [in mathcomp.algebra.vector]
-dirrE [in mathcomp.character.vcharacter]
-dIrrP [in mathcomp.character.vcharacter]
-dirrP [in mathcomp.character.vcharacter]
-dirr_small_norm [in mathcomp.character.vcharacter]
-dirr_constt_oppl [in mathcomp.character.vcharacter]
-dirr_constt_oppI [in mathcomp.character.vcharacter]
-dirr_constt_oppr [in mathcomp.character.vcharacter]
-dirr_consttE [in mathcomp.character.vcharacter]
-dirr_dIirrE [in mathcomp.character.vcharacter]
-dirr_dIirrPE [in mathcomp.character.vcharacter]
-dirr_inj [in mathcomp.character.vcharacter]
-dirr_dchi [in mathcomp.character.vcharacter]
-dirr_aut [in mathcomp.character.vcharacter]
-dirr_norm1 [in mathcomp.character.vcharacter]
-dirr_sign [in mathcomp.character.vcharacter]
-dirr_opp [in mathcomp.character.vcharacter]
-dirr_oppr_closed [in mathcomp.character.vcharacter]
-dirr_key [in mathcomp.character.vcharacter]
-dir_s0p [in mathcomp.solvable.burnside_app]
-dir_iso_iso3 [in mathcomp.solvable.burnside_app]
-disjoints_subset [in mathcomp.ssreflect.finset]
-disjointU [in mathcomp.ssreflect.fintype]
-disjointU1 [in mathcomp.ssreflect.fintype]
-disjoint_cat [in mathcomp.ssreflect.fintype]
-disjoint_has [in mathcomp.ssreflect.fintype]
-disjoint_cons [in mathcomp.ssreflect.fintype]
-disjoint_trans [in mathcomp.ssreflect.fintype]
-disjoint_subset [in mathcomp.ssreflect.fintype]
-disjoint_sym [in mathcomp.ssreflect.fintype]
-disjoint_setI0 [in mathcomp.ssreflect.finset]
-disjoint0 [in mathcomp.ssreflect.fintype]
-disjoint1 [in mathcomp.ssreflect.fintype]
-divgI [in mathcomp.fingroup.fingroup]
-divgrM [in mathcomp.fingroup.gproduct]
-divgrMid [in mathcomp.fingroup.gproduct]
-divgrMl [in mathcomp.fingroup.gproduct]
-divgr_id [in mathcomp.fingroup.gproduct]
-divgr_eq [in mathcomp.fingroup.gproduct]
-divgS [in mathcomp.fingroup.fingroup]
-divg_normal [in mathcomp.fingroup.quotient]
-divg_indexS [in mathcomp.fingroup.fingroup]
-divg_index [in mathcomp.fingroup.fingroup]
-divisors_id [in mathcomp.ssreflect.prime]
-divisors_uniq [in mathcomp.ssreflect.prime]
-divisors_correct [in mathcomp.ssreflect.prime]
-divisor1 [in mathcomp.ssreflect.prime]
-divnA [in mathcomp.ssreflect.div]
-divnAC [in mathcomp.ssreflect.div]
-divnDl [in mathcomp.ssreflect.div]
-divnDr [in mathcomp.ssreflect.div]
-divnK [in mathcomp.ssreflect.div]
-divnMA [in mathcomp.ssreflect.div]
-divnMDl [in mathcomp.ssreflect.div]
-divnMl [in mathcomp.ssreflect.div]
-divnMr [in mathcomp.ssreflect.div]
-divnn [in mathcomp.ssreflect.div]
-divNz_nat [in mathcomp.algebra.intdiv]
-divn_count_dvd [in mathcomp.ssreflect.prime]
-divn_mulAC [in mathcomp.ssreflect.div]
-divn_gt0 [in mathcomp.ssreflect.div]
-divn_small [in mathcomp.ssreflect.div]
-divn_eq [in mathcomp.ssreflect.div]
-divn0 [in mathcomp.ssreflect.div]
-divn1 [in mathcomp.ssreflect.div]
-divn2 [in mathcomp.ssreflect.div]
-divp_polyOver [in mathcomp.field.fieldext]
-divqP [in mathcomp.algebra.rat]
-divq_eq [in mathcomp.algebra.rat]
-divq_num_den [in mathcomp.algebra.rat]
-divzA [in mathcomp.algebra.intdiv]
-divzAC [in mathcomp.algebra.intdiv]
-divzDl [in mathcomp.algebra.intdiv]
-divzDr [in mathcomp.algebra.intdiv]
-divzK [in mathcomp.algebra.intdiv]
-divzMA [in mathcomp.algebra.intdiv]
-divzMA_ge0 [in mathcomp.algebra.intdiv]
-divzMDl [in mathcomp.algebra.intdiv]
-divzMl [in mathcomp.algebra.intdiv]
-divzMpl [in mathcomp.algebra.intdiv]
-divzMpr [in mathcomp.algebra.intdiv]
-divzMr [in mathcomp.algebra.intdiv]
-divzN [in mathcomp.algebra.intdiv]
-divzz [in mathcomp.algebra.intdiv]
-divz_mulAC [in mathcomp.algebra.intdiv]
-divz_ge0 [in mathcomp.algebra.intdiv]
-divz_small [in mathcomp.algebra.intdiv]
-divz_eq [in mathcomp.algebra.intdiv]
-divz_abs [in mathcomp.algebra.intdiv]
-divz_nat [in mathcomp.algebra.intdiv]
-divz0 [in mathcomp.algebra.intdiv]
-divz1 [in mathcomp.algebra.intdiv]
-div_annihilantP [in mathcomp.algebra.polyXY]
-div_annihilant_neq0 [in mathcomp.algebra.polyXY]
-div_annihilant_in_ideal [in mathcomp.algebra.polyXY]
-div_ring_mul_group_cyclic [in mathcomp.solvable.cyclic]
-div0n [in mathcomp.ssreflect.div]
-div0z [in mathcomp.algebra.intdiv]
-DnQ_extraspecial [in mathcomp.solvable.extraspecial]
-DnQ_pgroup [in mathcomp.solvable.extraspecial]
-DnQ_P [in mathcomp.solvable.extraspecial]
-domP [in mathcomp.fingroup.morphism]
-dom_hom_mx_module [in mathcomp.character.mxrepresentation]
-dom_hom_invmx [in mathcomp.character.mxrepresentation]
-dom_qactJ [in mathcomp.fingroup.action]
-dom_ker [in mathcomp.fingroup.morphism]
-doubleB [in mathcomp.ssreflect.ssrnat]
-doubleD [in mathcomp.ssreflect.ssrnat]
-doubleE [in mathcomp.ssreflect.ssrnat]
-doubleK [in mathcomp.ssreflect.ssrnat]
-doubleMl [in mathcomp.ssreflect.ssrnat]
-doubleMr [in mathcomp.ssreflect.ssrnat]
-doubleS [in mathcomp.ssreflect.ssrnat]
-double_eq0 [in mathcomp.ssreflect.ssrnat]
-double_gt0 [in mathcomp.ssreflect.ssrnat]
-double0 [in mathcomp.ssreflect.ssrnat]
-dprodA [in mathcomp.fingroup.gproduct]
-dprodC [in mathcomp.fingroup.gproduct]
-dprodE [in mathcomp.fingroup.gproduct]
-dprodEcp [in mathcomp.fingroup.gproduct]
-dprodEsd [in mathcomp.fingroup.gproduct]
-dprodEY [in mathcomp.fingroup.gproduct]
-dprodg1 [in mathcomp.fingroup.gproduct]
-dprodJ [in mathcomp.fingroup.gproduct]
-dprodl_Iirr0 [in mathcomp.character.character]
-dprodl_Iirr_eq0 [in mathcomp.character.character]
-dprodl_IirrK [in mathcomp.character.character]
-dprodl_IirrE [in mathcomp.character.character]
-dprodmE [in mathcomp.fingroup.gproduct]
-dprodmEl [in mathcomp.fingroup.gproduct]
-dprodmEr [in mathcomp.fingroup.gproduct]
-dprodm_eqf [in mathcomp.fingroup.gproduct]
-dprodm_cprod [in mathcomp.fingroup.gproduct]
-dprodP [in mathcomp.fingroup.gproduct]
-dprodr_Iirr0 [in mathcomp.character.character]
-dprodr_Iirr_eq0 [in mathcomp.character.character]
-dprodr_IirrK [in mathcomp.character.character]
-dprodr_IirrE [in mathcomp.character.character]
-dprodW [in mathcomp.fingroup.gproduct]
-dprodWC [in mathcomp.fingroup.gproduct]
-dprodWcp [in mathcomp.fingroup.gproduct]
-dprodWsd [in mathcomp.fingroup.gproduct]
-dprodWsdC [in mathcomp.fingroup.gproduct]
-dprodWY [in mathcomp.fingroup.gproduct]
-dprodYP [in mathcomp.fingroup.gproduct]
-dprod_card [in mathcomp.fingroup.gproduct]
-dprod_modr [in mathcomp.fingroup.gproduct]
-dprod_modl [in mathcomp.fingroup.gproduct]
-dprod_normal2 [in mathcomp.fingroup.gproduct]
-dprod_IirrC [in mathcomp.character.character]
-dprod_IirrK [in mathcomp.character.character]
-dprod_Iirr_onto [in mathcomp.character.character]
-dprod_Iirr_eq0 [in mathcomp.character.character]
-dprod_Iirr0r [in mathcomp.character.character]
-dprod_Iirr0l [in mathcomp.character.character]
-dprod_Iirr0 [in mathcomp.character.character]
-dprod_Iirr_inj [in mathcomp.character.character]
-dprod_IirrEr [in mathcomp.character.character]
-dprod_IirrEl [in mathcomp.character.character]
-dprod_IirrE [in mathcomp.character.character]
-dprod_homocyclic [in mathcomp.solvable.abelian]
-dprod_abelem [in mathcomp.solvable.abelian]
-dprod_exponent [in mathcomp.solvable.abelian]
-dprod_rowg [in mathcomp.character.mxabelem]
-dprod_nil [in mathcomp.solvable.nilpotent]
-dprod1g [in mathcomp.fingroup.gproduct]
-drop_tupleP [in mathcomp.ssreflect.tuple]
-drop_subseq [in mathcomp.ssreflect.seq]
-drop_rev [in mathcomp.ssreflect.seq]
-drop_nth [in mathcomp.ssreflect.seq]
-drop_rcons [in mathcomp.ssreflect.seq]
-drop_drop [in mathcomp.ssreflect.seq]
-drop_size_cat [in mathcomp.ssreflect.seq]
-drop_cat [in mathcomp.ssreflect.seq]
-drop_cons [in mathcomp.ssreflect.seq]
-drop_size [in mathcomp.ssreflect.seq]
-drop_oversize [in mathcomp.ssreflect.seq]
-drop_behead [in mathcomp.ssreflect.seq]
-drop0 [in mathcomp.ssreflect.seq]
-drop1 [in mathcomp.ssreflect.seq]
-dsubmx_key [in mathcomp.algebra.matrix]
-dsumx_mul [in mathcomp.character.character]
-dtuple_on_subset [in mathcomp.solvable.primitive_action]
-dtuple_on_add_D1 [in mathcomp.solvable.primitive_action]
-dtuple_on_add [in mathcomp.solvable.primitive_action]
-dtuple_onP [in mathcomp.solvable.primitive_action]
-dvdA_zmod_closed [in mathcomp.field.algnum]
-dvdA_key [in mathcomp.field.algnum]
-dvdCP [in mathcomp.field.algC]
-dvdCP_nat [in mathcomp.field.algC]
-dvdC_int [in mathcomp.field.algC]
-dvdC_nat [in mathcomp.field.algC]
-dvdC_zmod [in mathcomp.field.algC]
-dvdC_key [in mathcomp.field.algC]
-dvdC_refl [in mathcomp.field.algC]
-dvdC_trans [in mathcomp.field.algC]
-dvdC_mul2l [in mathcomp.field.algC]
-dvdC_mul2r [in mathcomp.field.algC]
-dvdC_mulr [in mathcomp.field.algC]
-dvdC_mull [in mathcomp.field.algC]
-dvdC0 [in mathcomp.field.algC]
-dvdnn [in mathcomp.ssreflect.div]
-dvdnP [in mathcomp.ssreflect.div]
-dvdn_quotient [in mathcomp.fingroup.quotient]
-dvdn_morphim [in mathcomp.fingroup.quotient]
-dvdn_pred_predX [in mathcomp.ssreflect.binomial]
-dvdn_partP [in mathcomp.ssreflect.prime]
-dvdn_sum [in mathcomp.ssreflect.prime]
-dvdn_divisors [in mathcomp.ssreflect.prime]
-dvdn_part [in mathcomp.ssreflect.prime]
-dvdn_pfactor [in mathcomp.ssreflect.prime]
-dvdn_leq_log [in mathcomp.ssreflect.prime]
-dvdn_prime2 [in mathcomp.ssreflect.prime]
-dvdn_pexp2r [in mathcomp.ssreflect.div]
-dvdn_double_ltn [in mathcomp.ssreflect.div]
-dvdn_double_leq [in mathcomp.ssreflect.div]
-dvdn_lcm [in mathcomp.ssreflect.div]
-dvdn_lcmr [in mathcomp.ssreflect.div]
-dvdn_lcml [in mathcomp.ssreflect.div]
-dvdn_gcd [in mathcomp.ssreflect.div]
-dvdn_gcdl [in mathcomp.ssreflect.div]
-dvdn_gcdr [in mathcomp.ssreflect.div]
-dvdn_fact [in mathcomp.ssreflect.div]
-dvdn_exp [in mathcomp.ssreflect.div]
-dvdn_sub [in mathcomp.ssreflect.div]
-dvdn_subl [in mathcomp.ssreflect.div]
-dvdn_subr [in mathcomp.ssreflect.div]
-dvdn_add_eq [in mathcomp.ssreflect.div]
-dvdn_add [in mathcomp.ssreflect.div]
-dvdn_addl [in mathcomp.ssreflect.div]
-dvdn_addr [in mathcomp.ssreflect.div]
-dvdn_exp2r [in mathcomp.ssreflect.div]
-dvdn_Pexp2l [in mathcomp.ssreflect.div]
-dvdn_exp2l [in mathcomp.ssreflect.div]
-dvdn_div [in mathcomp.ssreflect.div]
-dvdn_divRL [in mathcomp.ssreflect.div]
-dvdn_divLR [in mathcomp.ssreflect.div]
-dvdn_pmul2r [in mathcomp.ssreflect.div]
-dvdn_pmul2l [in mathcomp.ssreflect.div]
-dvdn_leq [in mathcomp.ssreflect.div]
-dvdn_odd [in mathcomp.ssreflect.div]
-dvdn_eq [in mathcomp.ssreflect.div]
-dvdn_trans [in mathcomp.ssreflect.div]
-dvdn_mul [in mathcomp.ssreflect.div]
-dvdn_mulr [in mathcomp.ssreflect.div]
-dvdn_mull [in mathcomp.ssreflect.div]
-dvdn_gt0 [in mathcomp.ssreflect.div]
-dvdn_orderC [in mathcomp.field.algnum]
-dvdn_constt_Res1_irr1 [in mathcomp.character.inertia]
-dvdn_exponent [in mathcomp.solvable.abelian]
-dvdn_orbit [in mathcomp.fingroup.action]
-dvdn_cforder [in mathcomp.character.classfun]
-dvdn_cforderP [in mathcomp.character.classfun]
-dvdn_prim_root [in mathcomp.algebra.poly]
-dvdn_biggcdP [in mathcomp.ssreflect.bigop]
-dvdn_biglcmP [in mathcomp.ssreflect.bigop]
-dvdn_cardMg [in mathcomp.fingroup.fingroup]
-dvdn_indexg [in mathcomp.fingroup.fingroup]
-dvdn_prime_cyclic [in mathcomp.solvable.cyclic]
-dvdn0 [in mathcomp.ssreflect.div]
-dvdn1 [in mathcomp.ssreflect.div]
-dvdn2 [in mathcomp.ssreflect.div]
-dvdpP_rat_int [in mathcomp.algebra.intdiv]
-dvdpP_int [in mathcomp.algebra.intdiv]
-dvdp_separable [in mathcomp.field.separable]
-dvdp_rat_int [in mathcomp.algebra.intdiv]
-dvdzE [in mathcomp.algebra.intdiv]
-dvdzP [in mathcomp.algebra.intdiv]
-dvdzz [in mathcomp.algebra.intdiv]
-dvdz_contents [in mathcomp.algebra.intdiv]
-dvdz_pexp2r [in mathcomp.algebra.intdiv]
-dvdz_gcd [in mathcomp.algebra.intdiv]
-dvdz_gcdl [in mathcomp.algebra.intdiv]
-dvdz_gcdr [in mathcomp.algebra.intdiv]
-dvdz_exp [in mathcomp.algebra.intdiv]
-dvdz_zmod_closed [in mathcomp.algebra.intdiv]
-dvdz_exp2r [in mathcomp.algebra.intdiv]
-dvdz_Pexp2l [in mathcomp.algebra.intdiv]
-dvdz_exp2l [in mathcomp.algebra.intdiv]
-dvdz_mul2r [in mathcomp.algebra.intdiv]
-dvdz_mul2l [in mathcomp.algebra.intdiv]
-dvdz_eq [in mathcomp.algebra.intdiv]
-dvdz_mod0P [in mathcomp.algebra.intdiv]
-dvdz_trans [in mathcomp.algebra.intdiv]
-dvdz_mul [in mathcomp.algebra.intdiv]
-dvdz_mulr [in mathcomp.algebra.intdiv]
-dvdz_mull [in mathcomp.algebra.intdiv]
-dvdz_key [in mathcomp.algebra.intdiv]
-dvdz0 [in mathcomp.algebra.intdiv]
-dvdz1 [in mathcomp.algebra.intdiv]
-dvd_irr1_index_center [in mathcomp.character.integral_char]
-dvd_irr1_cardG [in mathcomp.character.integral_char]
-dvd0C [in mathcomp.field.algC]
-dvd0n [in mathcomp.ssreflect.div]
-dvd0z [in mathcomp.algebra.intdiv]
-dvd1n [in mathcomp.ssreflect.div]
-dvd1z [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) | -