| 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) | +
E (lemma)
+ecubes_def [in mathcomp.solvable.burnside_app]+edivnP [in mathcomp.ssreflect.div]
+edivn_def [in mathcomp.ssreflect.div]
+edivn_eq [in mathcomp.ssreflect.div]
+edivn2P [in mathcomp.ssreflect.prime]
+egcdnP [in mathcomp.ssreflect.div]
+egcdzP [in mathcomp.algebra.intdiv]
+egcd0n [in mathcomp.ssreflect.div]
+eigenspaceP [in mathcomp.algebra.mxalgebra]
+eigenvalueP [in mathcomp.algebra.mxalgebra]
+eigenvalue_root_min [in mathcomp.algebra.mxpoly]
+eigenvalue_root_char [in mathcomp.algebra.mxpoly]
+eigenvalue_map [in mathcomp.algebra.mxalgebra]
+elogn2P [in mathcomp.ssreflect.prime]
+eltmE [in mathcomp.solvable.cyclic]
+eltmM [in mathcomp.solvable.cyclic]
+eltm_id [in mathcomp.solvable.cyclic]
+encoded_equivP [in mathcomp.ssreflect.generic_quotient]
+encoded_equiv_is_equiv [in mathcomp.ssreflect.generic_quotient]
+encoded_equivE [in mathcomp.ssreflect.generic_quotient]
+enc_mod_rel_is_equiv [in mathcomp.ssreflect.generic_quotient]
+enumP [in mathcomp.ssreflect.fintype]
+enumT [in mathcomp.ssreflect.fintype]
+enum_AEnd [in mathcomp.field.galois]
+enum_tupleP [in mathcomp.ssreflect.tuple]
+enum_ordS [in mathcomp.ssreflect.fintype]
+enum_val_ord [in mathcomp.ssreflect.fintype]
+enum_rank_ord [in mathcomp.ssreflect.fintype]
+enum_val_bij [in mathcomp.ssreflect.fintype]
+enum_rank_bij [in mathcomp.ssreflect.fintype]
+enum_val_bij_in [in mathcomp.ssreflect.fintype]
+enum_val_inj [in mathcomp.ssreflect.fintype]
+enum_rank_inj [in mathcomp.ssreflect.fintype]
+enum_valK [in mathcomp.ssreflect.fintype]
+enum_valK_in [in mathcomp.ssreflect.fintype]
+enum_rankK [in mathcomp.ssreflect.fintype]
+enum_rankK_in [in mathcomp.ssreflect.fintype]
+enum_val_nth [in mathcomp.ssreflect.fintype]
+enum_valP [in mathcomp.ssreflect.fintype]
+enum_default [in mathcomp.ssreflect.fintype]
+enum_rank_subproof [in mathcomp.ssreflect.fintype]
+enum_uniq [in mathcomp.ssreflect.fintype]
+enum_set1 [in mathcomp.ssreflect.finset]
+enum_setT [in mathcomp.ssreflect.finset]
+enum_set0 [in mathcomp.ssreflect.finset]
+enum0 [in mathcomp.ssreflect.fintype]
+enum1 [in mathcomp.ssreflect.fintype]
+envelop_mx_ring [in mathcomp.character.mxrepresentation]
+envelop_mxM [in mathcomp.character.mxrepresentation]
+envelop_mxP [in mathcomp.character.mxrepresentation]
+envelop_mx1 [in mathcomp.character.mxrepresentation]
+envelop_mx_id [in mathcomp.character.mxrepresentation]
+eqAmodD [in mathcomp.field.algnum]
+eqAmodDl [in mathcomp.field.algnum]
+eqAmodDr [in mathcomp.field.algnum]
+eqAmodM [in mathcomp.field.algnum]
+eqAmodMl [in mathcomp.field.algnum]
+eqAmodMl0 [in mathcomp.field.algnum]
+eqAmodMr [in mathcomp.field.algnum]
+eqAmodMr0 [in mathcomp.field.algnum]
+eqAmodm0 [in mathcomp.field.algnum]
+eqAmodN [in mathcomp.field.algnum]
+eqAmod_nat [in mathcomp.field.algnum]
+eqAmod_rat [in mathcomp.field.algnum]
+eqAmod_addl_mul [in mathcomp.field.algnum]
+eqAmod_transr [in mathcomp.field.algnum]
+eqAmod_transl [in mathcomp.field.algnum]
+eqAmod_trans [in mathcomp.field.algnum]
+eqAmod_sym [in mathcomp.field.algnum]
+eqAmod_refl [in mathcomp.field.algnum]
+eqAmod0 [in mathcomp.field.algnum]
+eqAmod0_nat [in mathcomp.field.algnum]
+eqAmod0_rat [in mathcomp.field.algnum]
+eqbE [in mathcomp.ssreflect.eqtype]
+eqbF_neg [in mathcomp.ssreflect.eqtype]
+eqbP [in mathcomp.ssreflect.eqtype]
+eqb_negLR [in mathcomp.ssreflect.eqtype]
+eqb_id [in mathcomp.ssreflect.eqtype]
+eqb0 [in mathcomp.ssreflect.ssrnat]
+eqb1 [in mathcomp.ssreflect.ssrnat]
+eqCmodD [in mathcomp.field.algC]
+eqCmodDl [in mathcomp.field.algC]
+eqCmodDr [in mathcomp.field.algC]
+eqCmodM [in mathcomp.field.algC]
+eqCmodMl [in mathcomp.field.algC]
+eqCmodMl0 [in mathcomp.field.algC]
+eqCmodMr [in mathcomp.field.algC]
+eqCmodMr0 [in mathcomp.field.algC]
+eqCmodm0 [in mathcomp.field.algC]
+eqCmodN [in mathcomp.field.algC]
+eqCmod_addl_mul [in mathcomp.field.algC]
+eqCmod_nat [in mathcomp.field.algC]
+eqCmod_transr [in mathcomp.field.algC]
+eqCmod_transl [in mathcomp.field.algC]
+eqCmod_trans [in mathcomp.field.algC]
+eqCmod_sym [in mathcomp.field.algC]
+eqCmod_refl [in mathcomp.field.algC]
+eqCmod0 [in mathcomp.field.algC]
+eqCmod0_nat [in mathcomp.field.algC]
+eqE [in mathcomp.ssreflect.eqtype]
+eqEcard [in mathcomp.ssreflect.finset]
+eqEdim [in mathcomp.algebra.vector]
+eqEproper [in mathcomp.ssreflect.finset]
+eqEsubset [in mathcomp.ssreflect.finset]
+eqEsubv [in mathcomp.algebra.vector]
+eqfunP [in mathcomp.ssreflect.fintype]
+eqfun_inP [in mathcomp.ssreflect.fintype]
+eqg_mx_abs_irr [in mathcomp.character.mxrepresentation]
+eqg_mx_irr [in mathcomp.character.mxrepresentation]
+eqg_mx_faithful [in mathcomp.character.mxrepresentation]
+eqg_repr_proof [in mathcomp.character.mxrepresentation]
+eqlfunP [in mathcomp.algebra.vector]
+eqlfun_inP [in mathcomp.algebra.vector]
+eqmodE [in mathcomp.ssreflect.generic_quotient]
+eqmodP [in mathcomp.ssreflect.generic_quotient]
+eqmxMfree [in mathcomp.algebra.mxalgebra]
+eqmxMfull [in mathcomp.algebra.mxalgebra]
+eqmxMr [in mathcomp.algebra.mxalgebra]
+eqmxP [in mathcomp.algebra.mxalgebra]
+eqmx_semisimple [in mathcomp.character.mxrepresentation]
+eqmx_iso [in mathcomp.character.mxrepresentation]
+eqmx_module [in mathcomp.character.mxrepresentation]
+eqmx_rstabs [in mathcomp.character.mxrepresentation]
+eqmx_rstab [in mathcomp.character.mxrepresentation]
+eqmx_sums [in mathcomp.algebra.mxalgebra]
+eqmx_conform [in mathcomp.algebra.mxalgebra]
+eqmx_cast [in mathcomp.algebra.mxalgebra]
+eqmx_opp [in mathcomp.algebra.mxalgebra]
+eqmx_scale [in mathcomp.algebra.mxalgebra]
+eqmx_rank [in mathcomp.algebra.mxalgebra]
+eqmx_trans [in mathcomp.algebra.mxalgebra]
+eqmx_sym [in mathcomp.algebra.mxalgebra]
+eqmx_refl [in mathcomp.algebra.mxalgebra]
+eqmx_eq0 [in mathcomp.algebra.mxalgebra]
+eqmx0 [in mathcomp.algebra.mxalgebra]
+eqmx0P [in mathcomp.algebra.mxalgebra]
+eqnE [in mathcomp.ssreflect.ssrnat]
+eqnP [in mathcomp.ssreflect.ssrnat]
+eqn_mod_dvd [in mathcomp.ssreflect.div]
+eqn_dvd [in mathcomp.ssreflect.div]
+eqn_mul [in mathcomp.ssreflect.div]
+eqn_div [in mathcomp.ssreflect.div]
+eqn_modDr [in mathcomp.ssreflect.div]
+eqn_modDl [in mathcomp.ssreflect.div]
+eqn_sqr [in mathcomp.ssreflect.ssrnat]
+eqn_exp2r [in mathcomp.ssreflect.ssrnat]
+eqn_exp2l [in mathcomp.ssreflect.ssrnat]
+eqn_pmul2r [in mathcomp.ssreflect.ssrnat]
+eqn_pmul2l [in mathcomp.ssreflect.ssrnat]
+eqn_mul2r [in mathcomp.ssreflect.ssrnat]
+eqn_mul2l [in mathcomp.ssreflect.ssrnat]
+eqn_leq [in mathcomp.ssreflect.ssrnat]
+eqn_add2r [in mathcomp.ssreflect.ssrnat]
+eqn_add2l [in mathcomp.ssreflect.ssrnat]
+eqn0Ngt [in mathcomp.ssreflect.ssrnat]
+eqP [in mathcomp.ssreflect.eqtype]
+eqperm [in mathcomp.solvable.burnside_app]
+eqperm_map2 [in mathcomp.solvable.burnside_app]
+eqperm_map [in mathcomp.solvable.burnside_app]
+eqp_separable [in mathcomp.field.separable]
+eqquotE [in mathcomp.ssreflect.generic_quotient]
+eqquotP [in mathcomp.ssreflect.generic_quotient]
+eqr_expz2 [in mathcomp.algebra.ssrint]
+eqr_int [in mathcomp.algebra.ssrint]
+eqseqE [in mathcomp.ssreflect.seq]
+eqseqP [in mathcomp.ssreflect.seq]
+eqseq_rot [in mathcomp.ssreflect.seq]
+eqseq_rcons [in mathcomp.ssreflect.seq]
+eqseq_cat [in mathcomp.ssreflect.seq]
+eqseq_cons [in mathcomp.ssreflect.seq]
+eqSS [in mathcomp.ssreflect.ssrnat]
+eqsVneq [in mathcomp.ssreflect.finset]
+equal_toE [in mathcomp.ssreflect.generic_quotient]
+equivalence_partition_pblock [in mathcomp.ssreflect.finset]
+equivalence_partitionP [in mathcomp.ssreflect.finset]
+EquivQuot.canon_id [in mathcomp.ssreflect.generic_quotient]
+EquivQuot.eqMixin [in mathcomp.ssreflect.generic_quotient]
+EquivQuot.eqmodE [in mathcomp.ssreflect.generic_quotient]
+EquivQuot.eqmodP [in mathcomp.ssreflect.generic_quotient]
+EquivQuot.equivQTP [in mathcomp.ssreflect.generic_quotient]
+EquivQuot.ereprK [in mathcomp.ssreflect.generic_quotient]
+EquivQuot.pi_DC [in mathcomp.ssreflect.generic_quotient]
+EquivQuot.pi_CD [in mathcomp.ssreflect.generic_quotient]
+equiv_subfext_is_equiv [in mathcomp.field.fieldext]
+equiv_rtrans [in mathcomp.ssreflect.generic_quotient]
+equiv_ltrans [in mathcomp.ssreflect.generic_quotient]
+equiv_trans [in mathcomp.ssreflect.generic_quotient]
+equiv_sym [in mathcomp.ssreflect.generic_quotient]
+equiv_refl [in mathcomp.ssreflect.generic_quotient]
+eqVneq [in mathcomp.ssreflect.eqtype]
+eqVproper [in mathcomp.ssreflect.finset]
+eqz_mod_dvd [in mathcomp.algebra.intdiv]
+eqz_mul [in mathcomp.algebra.intdiv]
+eqz_div [in mathcomp.algebra.intdiv]
+eqz_modDr [in mathcomp.algebra.intdiv]
+eqz_modDl [in mathcomp.algebra.intdiv]
+eqz_nat [in mathcomp.algebra.ssrint]
+eq_galP [in mathcomp.field.galois]
+eq_p'core [in mathcomp.solvable.pgroup]
+eq_pcore [in mathcomp.solvable.pgroup]
+eq_in_pcore [in mathcomp.solvable.pgroup]
+eq_Hall_pcore [in mathcomp.solvable.pgroup]
+eq_constt [in mathcomp.solvable.pgroup]
+eq_p_elt [in mathcomp.solvable.pgroup]
+eq_p'Hall [in mathcomp.solvable.pgroup]
+eq_pHall [in mathcomp.solvable.pgroup]
+eq_in_pHall [in mathcomp.solvable.pgroup]
+eq_p'group [in mathcomp.solvable.pgroup]
+eq_pgroup [in mathcomp.solvable.pgroup]
+eq_fcycle [in mathcomp.ssreflect.path]
+eq_fpath [in mathcomp.ssreflect.path]
+eq_sorted_irr [in mathcomp.ssreflect.path]
+eq_sorted [in mathcomp.ssreflect.path]
+eq_cycle [in mathcomp.ssreflect.path]
+eq_path [in mathcomp.ssreflect.path]
+eq_pcycle_mem [in mathcomp.fingroup.perm]
+eq_pnat [in mathcomp.ssreflect.prime]
+eq_in_pnat [in mathcomp.ssreflect.prime]
+eq_partn [in mathcomp.ssreflect.prime]
+eq_in_partn [in mathcomp.ssreflect.prime]
+eq_piP [in mathcomp.ssreflect.prime]
+eq_negn [in mathcomp.ssreflect.prime]
+eq_primes [in mathcomp.ssreflect.prime]
+eq_adjoin_separable_generator [in mathcomp.field.separable]
+eq_limg_ker0 [in mathcomp.algebra.vector]
+eq_in_limg [in mathcomp.algebra.vector]
+eq_span [in mathcomp.algebra.vector]
+eq_quot_countMixin [in mathcomp.ssreflect.generic_quotient]
+eq_op_trans [in mathcomp.ssreflect.generic_quotient]
+eq_lock [in mathcomp.ssreflect.generic_quotient]
+eq_from_tnth [in mathcomp.ssreflect.tuple]
+eq_block_mx [in mathcomp.algebra.matrix]
+eq_col_mx [in mathcomp.algebra.matrix]
+eq_row_mx [in mathcomp.algebra.matrix]
+eq_Aut [in mathcomp.fingroup.automorphism]
+eq_subZnat_irr [in mathcomp.character.character]
+eq_addZ_irr [in mathcomp.character.character]
+eq_scale_irr [in mathcomp.character.character]
+eq_signed_irr [in mathcomp.character.character]
+eq_scaled_irr [in mathcomp.character.character]
+eq_irr_mem_classP [in mathcomp.character.character]
+eq_sum_nth_irr [in mathcomp.character.character]
+eq_Mod8_D8 [in mathcomp.solvable.extremal]
+eq_from_flatten_shape [in mathcomp.ssreflect.seq]
+eq_mkseq [in mathcomp.ssreflect.seq]
+eq_pmap [in mathcomp.ssreflect.seq]
+eq_in_map [in mathcomp.ssreflect.seq]
+eq_map [in mathcomp.ssreflect.seq]
+eq_all_r [in mathcomp.ssreflect.seq]
+eq_has_r [in mathcomp.ssreflect.seq]
+eq_in_has [in mathcomp.ssreflect.seq]
+eq_in_all [in mathcomp.ssreflect.seq]
+eq_in_count [in mathcomp.ssreflect.seq]
+eq_in_find [in mathcomp.ssreflect.seq]
+eq_in_filter [in mathcomp.ssreflect.seq]
+eq_all [in mathcomp.ssreflect.seq]
+eq_has [in mathcomp.ssreflect.seq]
+eq_count [in mathcomp.ssreflect.seq]
+eq_filter [in mathcomp.ssreflect.seq]
+eq_find [in mathcomp.ssreflect.seq]
+eq_from_nth [in mathcomp.ssreflect.seq]
+eq_cfclass_IirrE [in mathcomp.character.inertia]
+eq_choose [in mathcomp.ssreflect.choice]
+eq_xchoose [in mathcomp.ssreflect.choice]
+eq_abelian_type_isog [in mathcomp.solvable.abelian]
+eq_homGrp [in mathcomp.fingroup.presentation]
+eq_card_prod [in mathcomp.ssreflect.fintype]
+eq_card_sub [in mathcomp.ssreflect.fintype]
+eq_invF [in mathcomp.ssreflect.fintype]
+eq_codom [in mathcomp.ssreflect.fintype]
+eq_image [in mathcomp.ssreflect.fintype]
+eq_forallb_in [in mathcomp.ssreflect.fintype]
+eq_forallb [in mathcomp.ssreflect.fintype]
+eq_existsb_in [in mathcomp.ssreflect.fintype]
+eq_existsb [in mathcomp.ssreflect.fintype]
+eq_disjoint1 [in mathcomp.ssreflect.fintype]
+eq_disjoint0 [in mathcomp.ssreflect.fintype]
+eq_disjoint_r [in mathcomp.ssreflect.fintype]
+eq_disjoint [in mathcomp.ssreflect.fintype]
+eq_proper_r [in mathcomp.ssreflect.fintype]
+eq_proper [in mathcomp.ssreflect.fintype]
+eq_subxx [in mathcomp.ssreflect.fintype]
+eq_subset_r [in mathcomp.ssreflect.fintype]
+eq_subset [in mathcomp.ssreflect.fintype]
+eq_card1 [in mathcomp.ssreflect.fintype]
+eq_cardT [in mathcomp.ssreflect.fintype]
+eq_card0 [in mathcomp.ssreflect.fintype]
+eq_card_trans [in mathcomp.ssreflect.fintype]
+eq_card [in mathcomp.ssreflect.fintype]
+eq_pick [in mathcomp.ssreflect.fintype]
+eq_enum [in mathcomp.ssreflect.fintype]
+eq_cfker_Res [in mathcomp.character.classfun]
+eq_orthonormal [in mathcomp.character.classfun]
+eq_pairwise_orthogonal [in mathcomp.character.classfun]
+eq_orthogonal [in mathcomp.character.classfun]
+eq_cfdotr [in mathcomp.character.classfun]
+eq_cfdotl [in mathcomp.character.classfun]
+eq_cfuni [in mathcomp.character.classfun]
+eq_mul_cfuni [in mathcomp.character.classfun]
+eq_binP [in mathcomp.ssreflect.ssrnat]
+eq_iterop [in mathcomp.ssreflect.ssrnat]
+eq_iteri [in mathcomp.ssreflect.ssrnat]
+eq_iter [in mathcomp.ssreflect.ssrnat]
+eq_ex_maxn [in mathcomp.ssreflect.ssrnat]
+eq_ex_minn [in mathcomp.ssreflect.ssrnat]
+eq_leq [in mathcomp.ssreflect.ssrnat]
+eq_map_poly [in mathcomp.algebra.poly]
+eq_prim_root_expr [in mathcomp.algebra.poly]
+eq_bigmax [in mathcomp.ssreflect.bigop]
+eq_bigmax_cond [in mathcomp.ssreflect.bigop]
+eq_big_idem [in mathcomp.ssreflect.bigop]
+eq_big_perm [in mathcomp.ssreflect.bigop]
+eq_big_idx [in mathcomp.ssreflect.bigop]
+eq_big_idx_seq [in mathcomp.ssreflect.bigop]
+eq_big_nat [in mathcomp.ssreflect.bigop]
+eq_big_seq [in mathcomp.ssreflect.bigop]
+eq_big [in mathcomp.ssreflect.bigop]
+eq_bigr [in mathcomp.ssreflect.bigop]
+eq_bigl [in mathcomp.ssreflect.bigop]
+eq_big_op [in mathcomp.ssreflect.bigop]
+eq_Tagged [in mathcomp.ssreflect.eqtype]
+eq_tag [in mathcomp.ssreflect.eqtype]
+eq_frel [in mathcomp.ssreflect.eqtype]
+eq_axiomK [in mathcomp.ssreflect.eqtype]
+eq_irrelevance [in mathcomp.ssreflect.eqtype]
+eq_sym [in mathcomp.ssreflect.eqtype]
+eq_refl [in mathcomp.ssreflect.eqtype]
+eq_abelem_subg_repr [in mathcomp.character.mxabelem]
+eq_rowg [in mathcomp.character.mxabelem]
+eq_homgr [in mathcomp.fingroup.morphism]
+eq_homgl [in mathcomp.fingroup.morphism]
+eq_in_morphim [in mathcomp.fingroup.morphism]
+eq_morphim [in mathcomp.fingroup.morphism]
+eq_mulVg1 [in mathcomp.fingroup.fingroup]
+eq_mulgV1 [in mathcomp.fingroup.fingroup]
+eq_invg_mul [in mathcomp.fingroup.fingroup]
+eq_invg1 [in mathcomp.fingroup.fingroup]
+eq_invg_sym [in mathcomp.fingroup.fingroup]
+eq_cpairZ [in mathcomp.solvable.center]
+eq_froots [in mathcomp.ssreflect.fingraph]
+eq_froot [in mathcomp.ssreflect.fingraph]
+eq_finv [in mathcomp.ssreflect.fingraph]
+eq_fcard [in mathcomp.ssreflect.fingraph]
+eq_fconnect [in mathcomp.ssreflect.fingraph]
+eq_roots [in mathcomp.ssreflect.fingraph]
+eq_root [in mathcomp.ssreflect.fingraph]
+eq_n_comp_r [in mathcomp.ssreflect.fingraph]
+eq_n_comp [in mathcomp.ssreflect.fingraph]
+eq_connect [in mathcomp.ssreflect.fingraph]
+eq_connect0 [in mathcomp.ssreflect.fingraph]
+eq_subG_cyclic [in mathcomp.solvable.cyclic]
+eq_expg_mod_order [in mathcomp.solvable.cyclic]
+eq_rank_unitmx [in mathcomp.algebra.mxalgebra]
+eq_genmx [in mathcomp.algebra.mxalgebra]
+eq_row_base [in mathcomp.algebra.mxalgebra]
+eq_row_sub [in mathcomp.algebra.mxalgebra]
+eq_pblock [in mathcomp.ssreflect.finset]
+eq_in_imset2 [in mathcomp.ssreflect.finset]
+eq_in_imset [in mathcomp.ssreflect.finset]
+eq_imset [in mathcomp.ssreflect.finset]
+eq_preimset [in mathcomp.ssreflect.finset]
+Euclid_dvdX [in mathcomp.ssreflect.prime]
+Euclid_dvd1 [in mathcomp.ssreflect.prime]
+Euclid_dvdM [in mathcomp.ssreflect.prime]
+Euler_exp_totient [in mathcomp.solvable.cyclic]
+eval_mxmodule [in mathcomp.character.mxrepresentation]
+eval_poly1 [in mathcomp.field.closed_field]
+eval_poly_mulM [in mathcomp.field.closed_field]
+eval_natmulpT [in mathcomp.field.closed_field]
+eval_opppT [in mathcomp.field.closed_field]
+eval_mulpT [in mathcomp.field.closed_field]
+eval_sumpT [in mathcomp.field.closed_field]
+eval_amulXnT [in mathcomp.field.closed_field]
+eval_lift [in mathcomp.field.closed_field]
+even_prime [in mathcomp.ssreflect.prime]
+exchange_big_nat [in mathcomp.ssreflect.bigop]
+exchange_big_dep_nat [in mathcomp.ssreflect.bigop]
+exchange_big [in mathcomp.ssreflect.bigop]
+exchange_big_dep [in mathcomp.ssreflect.bigop]
+existsb_tnth [in mathcomp.ssreflect.tuple]
+existsP [in mathcomp.ssreflect.fintype]
+existsPP [in mathcomp.ssreflect.fintype]
+exists_acomps [in mathcomp.solvable.jordanholder]
+exists_comps [in mathcomp.solvable.jordanholder]
+exists_eq_inP [in mathcomp.ssreflect.fintype]
+exists_inP [in mathcomp.ssreflect.fintype]
+exists_eqP [in mathcomp.ssreflect.fintype]
+expand_det_col [in mathcomp.algebra.matrix]
+expand_det_row [in mathcomp.algebra.matrix]
+expand_cofactor [in mathcomp.algebra.matrix]
+expfV [in mathcomp.algebra.ssrint]
+expfzDr [in mathcomp.algebra.ssrint]
+expfzMl [in mathcomp.algebra.ssrint]
+expfz_n0addr [in mathcomp.algebra.ssrint]
+expfz_neq0 [in mathcomp.algebra.ssrint]
+expfz_eq0 [in mathcomp.algebra.ssrint]
+expf_card [in mathcomp.field.finfield]
+expgAC [in mathcomp.fingroup.fingroup]
+expgD [in mathcomp.fingroup.fingroup]
+expgK [in mathcomp.solvable.cyclic]
+expgM [in mathcomp.fingroup.fingroup]
+expgMn [in mathcomp.fingroup.fingroup]
+expgnE [in mathcomp.fingroup.fingroup]
+expgS [in mathcomp.fingroup.fingroup]
+expgSr [in mathcomp.fingroup.fingroup]
+expgVn [in mathcomp.fingroup.fingroup]
+expg_exponent [in mathcomp.solvable.abelian]
+expg_mod_order [in mathcomp.fingroup.fingroup]
+expg_mod [in mathcomp.fingroup.fingroup]
+expg_order [in mathcomp.fingroup.fingroup]
+expg_zneg [in mathcomp.solvable.cyclic]
+expg_znat [in mathcomp.solvable.cyclic]
+expg_cardG [in mathcomp.solvable.cyclic]
+expg0 [in mathcomp.fingroup.fingroup]
+expg1 [in mathcomp.fingroup.fingroup]
+expg1n [in mathcomp.fingroup.fingroup]
+expIn [in mathcomp.ssreflect.ssrnat]
+expMg_Rmul [in mathcomp.solvable.commutator]
+expnAC [in mathcomp.ssreflect.ssrnat]
+expnB [in mathcomp.ssreflect.div]
+expnD [in mathcomp.ssreflect.ssrnat]
+expnE [in mathcomp.ssreflect.ssrnat]
+expnI [in mathcomp.ssreflect.ssrnat]
+expnM [in mathcomp.ssreflect.ssrnat]
+expnMn [in mathcomp.ssreflect.ssrnat]
+expNrz [in mathcomp.algebra.ssrint]
+expnS [in mathcomp.ssreflect.ssrnat]
+expnSr [in mathcomp.ssreflect.ssrnat]
+expn_max [in mathcomp.ssreflect.div]
+expn_min [in mathcomp.ssreflect.div]
+expn_eq0 [in mathcomp.ssreflect.ssrnat]
+expn_gt0 [in mathcomp.ssreflect.ssrnat]
+expn_sum [in mathcomp.ssreflect.bigop]
+expn0 [in mathcomp.ssreflect.ssrnat]
+expn1 [in mathcomp.ssreflect.ssrnat]
+expN1r [in mathcomp.algebra.ssrint]
+exponentJ [in mathcomp.solvable.abelian]
+exponentP [in mathcomp.solvable.abelian]
+exponentS [in mathcomp.solvable.abelian]
+exponent_pX1p2n [in mathcomp.solvable.extraspecial]
+exponent_pX1p2 [in mathcomp.solvable.extraspecial]
+exponent_dprod_homocyclic [in mathcomp.solvable.abelian]
+exponent_quotient [in mathcomp.solvable.abelian]
+exponent_isog [in mathcomp.solvable.abelian]
+exponent_injm [in mathcomp.solvable.abelian]
+exponent_morphim [in mathcomp.solvable.abelian]
+exponent_Zgroup [in mathcomp.solvable.abelian]
+exponent_Hall [in mathcomp.solvable.abelian]
+exponent_cyclic [in mathcomp.solvable.abelian]
+exponent_cycle [in mathcomp.solvable.abelian]
+exponent_witness [in mathcomp.solvable.abelian]
+exponent_gt0 [in mathcomp.solvable.abelian]
+exponent_dvdn [in mathcomp.solvable.abelian]
+exponent_Ohm1_class2 [in mathcomp.solvable.maximal]
+exponent_2extraspecial [in mathcomp.solvable.maximal]
+exponent_special [in mathcomp.solvable.maximal]
+exponent_mx_group [in mathcomp.character.mxabelem]
+exponent1 [in mathcomp.solvable.abelian]
+exponent2_abelem [in mathcomp.solvable.abelian]
+exprMz_comm [in mathcomp.algebra.ssrint]
+exprnN [in mathcomp.algebra.ssrint]
+exprnP [in mathcomp.algebra.ssrint]
+exprN1 [in mathcomp.algebra.ssrint]
+exprSz [in mathcomp.algebra.ssrint]
+exprSzr [in mathcomp.algebra.ssrint]
+exprzAC [in mathcomp.algebra.ssrint]
+exprzDr [in mathcomp.algebra.ssrint]
+exprzD_ss [in mathcomp.algebra.ssrint]
+exprzD_Nnat [in mathcomp.algebra.ssrint]
+exprzD_nat [in mathcomp.algebra.ssrint]
+exprzMl [in mathcomp.algebra.ssrint]
+exprzMzl [in mathcomp.algebra.ssrint]
+exprz_gt0 [in mathcomp.algebra.ssrint]
+exprz_ge0 [in mathcomp.algebra.ssrint]
+exprz_pintl [in mathcomp.algebra.ssrint]
+exprz_pmulzl [in mathcomp.algebra.ssrint]
+exprz_out [in mathcomp.algebra.ssrint]
+exprz_exp [in mathcomp.algebra.ssrint]
+exprz_inv [in mathcomp.algebra.ssrint]
+expr0z [in mathcomp.algebra.ssrint]
+expr1z [in mathcomp.algebra.ssrint]
+expS_cfunE [in mathcomp.character.classfun]
+expvD [in mathcomp.field.falgebra]
+expvM [in mathcomp.field.falgebra]
+expvS [in mathcomp.field.falgebra]
+expvSl [in mathcomp.field.falgebra]
+expvSr [in mathcomp.field.falgebra]
+expv_id [in mathcomp.field.falgebra]
+expv_line [in mathcomp.field.falgebra]
+expv0 [in mathcomp.field.falgebra]
+expv0n [in mathcomp.field.falgebra]
+expv1 [in mathcomp.field.falgebra]
+expv1n [in mathcomp.field.falgebra]
+expv2 [in mathcomp.field.falgebra]
+expzB [in mathcomp.algebra.intdiv]
+expz_min [in mathcomp.algebra.intdiv]
+exp_orderC [in mathcomp.field.algnum]
+exp_cforder [in mathcomp.character.classfun]
+exp_cfunE [in mathcomp.character.classfun]
+exp_prim_root [in mathcomp.algebra.poly]
+exp0n [in mathcomp.ssreflect.ssrnat]
+exp0rz [in mathcomp.algebra.ssrint]
+exp1n [in mathcomp.ssreflect.ssrnat]
+exp1rz [in mathcomp.algebra.ssrint]
+extendDerivationP [in mathcomp.field.separable]
+extendDerivation_horner [in mathcomp.field.separable]
+extendDerivation_id [in mathcomp.field.separable]
+extendDerivation_subproof [in mathcomp.field.separable]
+extendible_irr_invariant [in mathcomp.character.inertia]
+extend_group_splitting_field [in mathcomp.character.mxrepresentation]
+extend_algC_subfield_aut [in mathcomp.field.algnum]
+extend_solvable_coprime_irr [in mathcomp.character.inertia]
+extend_coprime_linear_char [in mathcomp.character.inertia]
+extend_linear_char_from_Sylow [in mathcomp.character.inertia]
+extend_to_cfdet [in mathcomp.character.inertia]
+extend_cyclic_Mho [in mathcomp.solvable.abelian]
+extend_cfConjC_subset [in mathcomp.character.classfun]
+external_action_im_coprime [in mathcomp.solvable.hall]
+extprod_mulgA [in mathcomp.fingroup.gproduct]
+extprod_mulVg [in mathcomp.fingroup.gproduct]
+extprod_mul1g [in mathcomp.fingroup.gproduct]
+extraspecial_structure [in mathcomp.solvable.maximal]
+extraspecial_nonabelian [in mathcomp.solvable.maximal]
+extraspecial_prime [in mathcomp.solvable.maximal]
+extraspecial_repr_structure [in mathcomp.character.mxabelem]
+extremal_generators_facts [in mathcomp.solvable.extremal]
+Extremal.act_dom [in mathcomp.solvable.extremal]
+Extremal.aut_dvdn [in mathcomp.solvable.extremal]
+Extremal.card [in mathcomp.solvable.extremal]
+Extremal.Grp [in mathcomp.solvable.extremal]
+Extremal.gtype_key [in mathcomp.solvable.extremal]
+extremal2_structure [in mathcomp.solvable.extremal]
+ext_coprime_quotient_cent [in mathcomp.solvable.hall]
+ext_coprime_Hall_subset [in mathcomp.solvable.hall]
+ext_norm_conj_cent [in mathcomp.solvable.hall]
+ext_coprime_Hall_trans [in mathcomp.solvable.hall]
+ext_coprime_Hall_exists [in mathcomp.solvable.hall]
+ex_maxnormal_ntrivg [in mathcomp.solvable.gseries]
+ex_maxnP [in mathcomp.ssreflect.ssrnat]
+ex_maxn_subproof [in mathcomp.ssreflect.ssrnat]
+ex_minnP [in mathcomp.ssreflect.ssrnat]
+ex_elim_qf [in mathcomp.field.closed_field]
+ex_elim_seq_qf [in mathcomp.field.closed_field]
+ex_elim_seqP [in mathcomp.field.closed_field]
+ex_mingroup [in mathcomp.fingroup.fingroup]
+ex_maxgroup [in mathcomp.fingroup.fingroup]
+ex_maxset [in mathcomp.ssreflect.finset]
+ex_minset [in mathcomp.ssreflect.finset]
+
| 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) | +