| 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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 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]
+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]
+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]
+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_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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +