| 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) | -
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]
-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]
-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]
-eqitvP [in mathcomp.algebra.interval]
-eqlfunP [in mathcomp.algebra.vector]
-eqlfun_inP [in mathcomp.algebra.vector]
-eqMixin [in mathcomp.ssreflect.finfun]
-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]
-eqmxMunitP [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_itv_boundP [in mathcomp.algebra.interval]
-eq_mktuple [in mathcomp.ssreflect.tuple]
-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_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_in_allpairs [in mathcomp.ssreflect.seq]
-eq_in_allpairs_dep [in mathcomp.ssreflect.seq]
-eq_allpairs [in mathcomp.ssreflect.seq]
-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_uniq [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_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_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_ffun [in mathcomp.ssreflect.finfun]
-eq_dffun [in mathcomp.ssreflect.finfun]
-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]
-eq_finset [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]
-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_inPP [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]
-extremumP [in mathcomp.ssreflect.fintype]
-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_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 | -(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) | -