E (Global Index)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
E
e [abbrev, in mathcomp.algebra.matrix]e' [abbrev, in mathcomp.boot.generic_quotient]
e'E [abbrev, in mathcomp.boot.generic_quotient]
e0 [abbrev, in mathcomp.group_representation.mxrepresentation]
E_ [abbrev, in mathcomp.group_representation.mxrepresentation]
E_G [abbrev, in mathcomp.group_representation.mxrepresentation]
E_G [abbrev, in mathcomp.group_representation.mxrepresentation]
E_G [abbrev, in mathcomp.group_representation.mxrepresentation]
eC [abbrev, in mathcomp.boot.generic_quotient]
ecubes [def, in mathcomp.solvable.burnside_app]
ecubes_def [prf, in mathcomp.solvable.burnside_app]
ED [abbrev, in mathcomp.solvable.extremal]
edivn [def, in mathcomp.boot.div]
edivn_def [prf, in mathcomp.boot.div]
edivn_eq [prf, in mathcomp.boot.div]
edivn_pred [prf, in mathcomp.boot.div]
edivn_rec [def, in mathcomp.boot.div]
edivn_spec [ind, in mathcomp.boot.div]
edivnB [prf, in mathcomp.boot.div]
edivnD [prf, in mathcomp.boot.div]
edivnP [prf, in mathcomp.boot.div]
edivnS [prf, in mathcomp.boot.div]
EdivnSpec [constr, in mathcomp.boot.div]
egcd0n [prf, in mathcomp.boot.div]
egcdn [def, in mathcomp.boot.div]
egcdn_rec [def, in mathcomp.boot.div]
egcdn_spec [ind, in mathcomp.boot.div]
egcdnP [prf, in mathcomp.boot.div]
EgcdnSpec [constr, in mathcomp.boot.div]
egcdz [def, in mathcomp.algebra.intdiv]
egcdz_spec [ind, in mathcomp.algebra.intdiv]
egcdzP [prf, in mathcomp.algebra.intdiv]
EgcdzSpec [constr, in mathcomp.algebra.intdiv]
eigenpoly [def, in mathcomp.algebra.mxpoly]
eigenpoly_conjmx [prf, in mathcomp.algebra.mxred]
eigenpoly_conjmx [prf, in mathcomp.algebra.mxpoly]
eigenpoly_map [prf, in mathcomp.algebra.mxpoly]
eigenpolyP [prf, in mathcomp.algebra.mxpoly]
eigenspace [def, in mathcomp.algebra.mxalgebra]
eigenspace_poly [prf, in mathcomp.algebra.mxpoly]
eigenspace_sub_geigen [prf, in mathcomp.algebra.mxpoly]
eigenspaceP [prf, in mathcomp.algebra.mxalgebra]
eigenvalue [def, in mathcomp.algebra.mxalgebra]
eigenvalue_closed [prf, in mathcomp.algebra.spectral]
eigenvalue_conjmx [prf, in mathcomp.algebra.mxred]
eigenvalue_conjmx [prf, in mathcomp.algebra.mxpoly]
eigenvalue_map [prf, in mathcomp.algebra.mxalgebra]
eigenvalue_poly [prf, in mathcomp.algebra.mxpoly]
eigenvalue_root_char [prf, in mathcomp.algebra.mxpoly]
eigenvalue_root_min [prf, in mathcomp.algebra.mxpoly]
eigenvalueP [prf, in mathcomp.algebra.mxalgebra]
eigenvectorP [prf, in mathcomp.algebra.mxalgebra]
eisenstein_crit [prf, in mathcomp.algebra.rat]
eltm [def, in mathcomp.solvable.cyclic]
eltm_id [prf, in mathcomp.solvable.cyclic]
eltm_morphism [def, in mathcomp.solvable.cyclic]
eltmE [prf, in mathcomp.solvable.cyclic]
eltmM [prf, in mathcomp.solvable.cyclic]
empty_itv [def, in mathcomp.algebra.interval_inference]
enc_mod_rel [proj, in mathcomp.boot.generic_quotient]
enc_mod_rel_equiv_rel [def, in mathcomp.boot.generic_quotient]
enc_mod_rel_is_equiv [prf, in mathcomp.boot.generic_quotient]
encModEquivP [def, in mathcomp.boot.generic_quotient]
EncModRel [abbrev, in mathcomp.boot.generic_quotient]
encModRel [rec, in mathcomp.boot.generic_quotient]
encModRel_class_of [ind, in mathcomp.boot.generic_quotient]
EncModRelClass [abbrev, in mathcomp.boot.generic_quotient]
encModRelClass [def, in mathcomp.boot.generic_quotient]
EncModRelClassPack [constr, in mathcomp.boot.generic_quotient]
encModRelE [def, in mathcomp.boot.generic_quotient]
encModRelP [def, in mathcomp.boot.generic_quotient]
encoded_equiv [def, in mathcomp.boot.generic_quotient]
encoded_equiv_equiv_rel [def, in mathcomp.boot.generic_quotient]
encoded_equiv_is_equiv [prf, in mathcomp.boot.generic_quotient]
encoded_equivE [prf, in mathcomp.boot.generic_quotient]
encoded_equivP [prf, in mathcomp.boot.generic_quotient]
enum [abbrev, in mathcomp.boot.fintype]
enum0 [prf, in mathcomp.boot.fintype]
enum1 [prf, in mathcomp.boot.fintype]
enum_AEnd [prf, in mathcomp.field.galois]
enum_default [prf, in mathcomp.boot.fintype]
enum_extremal_groups [def, in mathcomp.solvable.extremal]
enum_mem [def, in mathcomp.boot.fintype]
enum_ord0 [prf, in mathcomp.boot.fintype]
enum_ordSl [prf, in mathcomp.boot.fintype]
enum_ordSr [prf, in mathcomp.boot.fintype]
enum_rank [def, in mathcomp.boot.fintype]
enum_rank_bij [prf, in mathcomp.boot.fintype]
enum_rank_in [abbrev, in mathcomp.boot.fintype]
enum_rank_in [mod, in mathcomp.boot.fintype]
enum_rank_in.body [def, in mathcomp.boot.fintype]
enum_rank_in.unlock [def, in mathcomp.boot.fintype]
enum_rank_in_inj [prf, in mathcomp.boot.fintype]
enum_rank_in_Locked [modtype, in mathcomp.boot.fintype]
enum_rank_in_Locked.body [ax, in mathcomp.boot.fintype]
enum_rank_in_Locked.unlock [ax, in mathcomp.boot.fintype]
enum_rank_in_unlock_subterm [def, in mathcomp.boot.fintype]
enum_rank_inj [prf, in mathcomp.boot.fintype]
enum_rank_ord [prf, in mathcomp.boot.fintype]
enum_rankK [prf, in mathcomp.boot.fintype]
enum_rankK_in [prf, in mathcomp.boot.fintype]
enum_set0 [prf, in mathcomp.boot.finset]
enum_set1 [prf, in mathcomp.boot.finset]
enum_setI [prf, in mathcomp.boot.finset]
enum_setT [prf, in mathcomp.boot.finset]
enum_setU [prf, in mathcomp.boot.finset]
enum_subdef [def, in mathcomp.boot.fintype]
enum_tuple [def, in mathcomp.boot.tuple]
enum_tupleP [prf, in mathcomp.boot.tuple]
enum_uniq [prf, in mathcomp.boot.fintype]
enum_val [def, in mathcomp.boot.fintype]
enum_val_bij [prf, in mathcomp.boot.fintype]
enum_val_bij_in [prf, in mathcomp.boot.fintype]
enum_val_inj [prf, in mathcomp.boot.fintype]
enum_val_nth [prf, in mathcomp.boot.fintype]
enum_val_ord [prf, in mathcomp.boot.fintype]
enum_valK [prf, in mathcomp.boot.fintype]
enum_valK_in [prf, in mathcomp.boot.fintype]
enum_valP [prf, in mathcomp.boot.fintype]
enumF [abbrev, in mathcomp.boot.fintype]
enumP [prf, in mathcomp.boot.fintype]
enumP_subdef [def, in mathcomp.boot.fintype]
enumT [prf, in mathcomp.boot.fintype]
envelop_mx1 [prf, in mathcomp.group_representation.mxrepresentation]
envelop_mx_id [prf, in mathcomp.group_representation.mxrepresentation]
envelop_mx_ring [prf, in mathcomp.group_representation.mxrepresentation]
envelop_mxM [prf, in mathcomp.group_representation.mxrepresentation]
envelop_mxP [prf, in mathcomp.group_representation.mxrepresentation]
enveloping_algebra_mx [def, in mathcomp.group_representation.mxrepresentation]
eq0_subset [prf, in mathcomp.boot.finset]
eq0F [prf, in mathcomp.algebra.interval_inference]
Eq0NotPos [constr, in mathcomp.boot.ssrnat]
eq_abelem_subg_repr [prf, in mathcomp.group_representation.mxabelem]
eq_abelian_type_isog [prf, in mathcomp.solvable.abelian]
eq_addZ_irr [prf, in mathcomp.group_representation.character]
eq_adjoin_separable_generator [prf, in mathcomp.field.separable]
eq_all [prf, in mathcomp.boot.seq]
eq_all_r [prf, in mathcomp.boot.seq]
eq_allpairs [prf, in mathcomp.boot.seq]
eq_allpairsr [prf, in mathcomp.boot.seq]
eq_allrel [prf, in mathcomp.boot.seq]
eq_allrel_mem2 [prf, in mathcomp.boot.seq]
eq_allrel_meml [prf, in mathcomp.boot.seq]
eq_allrel_memr [prf, in mathcomp.boot.seq]
eq_Aut [prf, in mathcomp.finite_group.automorphism]
eq_axiom [def, in mathcomp.boot.eqtype]
eq_axiomK [prf, in mathcomp.boot.eqtype]
eq_big [prf, in mathcomp.boot.bigop]
eq_big_idem [prf, in mathcomp.boot.bigop]
eq_big_idx [prf, in mathcomp.boot.bigop]
eq_big_idx_seq [prf, in mathcomp.boot.bigop]
eq_big_nat [prf, in mathcomp.boot.bigop]
eq_big_op [prf, in mathcomp.boot.bigop]
eq_big_seq [prf, in mathcomp.boot.bigop]
eq_bigl [prf, in mathcomp.boot.bigop]
eq_bigl_supp [prf, in mathcomp.boot.bigop]
eq_bigmax [prf, in mathcomp.boot.bigop]
eq_bigmax_cond [prf, in mathcomp.boot.bigop]
eq_bigr [prf, in mathcomp.boot.bigop]
eq_binP [prf, in mathcomp.boot.ssrnat]
eq_block_mx [prf, in mathcomp.algebra.matrix]
eq_card [prf, in mathcomp.boot.fintype]
eq_card0 [prf, in mathcomp.boot.fintype]
eq_card1 [prf, in mathcomp.boot.fintype]
eq_card_prod [prf, in mathcomp.boot.fintype]
eq_card_sub [prf, in mathcomp.boot.fintype]
eq_card_trans [prf, in mathcomp.boot.fintype]
eq_cardT [prf, in mathcomp.boot.fintype]
eq_castmx [prf, in mathcomp.algebra.matrix]
eq_cfclass_IirrE [prf, in mathcomp.group_representation.inertia]
eq_cfdotl [prf, in mathcomp.group_representation.classfun]
eq_cfdotr [prf, in mathcomp.group_representation.classfun]
eq_cfker_Res [prf, in mathcomp.group_representation.classfun]
eq_cfuni [prf, in mathcomp.group_representation.classfun]
eq_choose [prf, in mathcomp.boot.choice]
eq_codom [prf, in mathcomp.boot.fintype]
eq_col_mx [prf, in mathcomp.algebra.matrix]
eq_colsub [prf, in mathcomp.algebra.matrix]
eq_comparable [def, in mathcomp.boot.eqtype]
eq_connect [prf, in mathcomp.boot.fingraph]
eq_connect0 [prf, in mathcomp.boot.fingraph]
eq_constt [prf, in mathcomp.solvable.pgroup]
eq_count [prf, in mathcomp.boot.seq]
eq_count_merge [prf, in mathcomp.boot.path]
eq_count_undup [prf, in mathcomp.boot.seq]
eq_cpairZ [prf, in mathcomp.solvable.center]
eq_cycle [prf, in mathcomp.boot.path]
eq_dffun [prf, in mathcomp.boot.finfun]
eq_dim_orthov1 [prf, in mathcomp.algebra.sesquilinear]
eq_dinjectiveb [prf, in mathcomp.boot.fintype]
eq_disjoint [prf, in mathcomp.boot.fintype]
eq_disjoint0 [prf, in mathcomp.boot.fintype]
eq_disjoint1 [prf, in mathcomp.boot.fintype]
eq_disjoint_r [prf, in mathcomp.boot.fintype]
eq_enum [prf, in mathcomp.boot.fintype]
eq_enum_rank_in [prf, in mathcomp.boot.fintype]
eq_ex_maxn [prf, in mathcomp.boot.ssrnat]
eq_ex_minn [prf, in mathcomp.boot.ssrnat]
eq_existsb [prf, in mathcomp.boot.fintype]
eq_existsb_in [prf, in mathcomp.boot.fintype]
eq_expg_mod_order [prf, in mathcomp.solvable.cyclic]
eq_expg_ord [prf, in mathcomp.solvable.cyclic]
eq_fcard [prf, in mathcomp.boot.fingraph]
eq_fconnect [prf, in mathcomp.boot.fingraph]
eq_fcycle [prf, in mathcomp.boot.path]
eq_ffun [prf, in mathcomp.boot.finfun]
eq_filter [prf, in mathcomp.boot.seq]
eq_find [prf, in mathcomp.boot.seq]
eq_finset [prf, in mathcomp.boot.finset]
eq_finv [prf, in mathcomp.boot.fingraph]
eq_forallb [prf, in mathcomp.boot.fintype]
eq_forallb_in [prf, in mathcomp.boot.fintype]
eq_fpath [prf, in mathcomp.boot.path]
eq_frel [prf, in mathcomp.boot.eqtype]
eq_from_flatten_shape [prf, in mathcomp.boot.seq]
eq_from_nth [prf, in mathcomp.boot.seq]
eq_from_onth [prf, in mathcomp.boot.seq]
eq_from_onth_le [prf, in mathcomp.boot.seq]
eq_from_Tagged [prf, in mathcomp.boot.eqtype]
eq_from_tnth [prf, in mathcomp.boot.tuple]
eq_froot [prf, in mathcomp.boot.fingraph]
eq_froots [prf, in mathcomp.boot.fingraph]
eq_fullrowsub [prf, in mathcomp.algebra.mxalgebra]
eq_galP [prf, in mathcomp.field.galois]
eq_genmx [prf, in mathcomp.algebra.mxalgebra]
eq_Hall_pcore [prf, in mathcomp.solvable.pgroup]
eq_has [prf, in mathcomp.boot.seq]
eq_has_r [prf, in mathcomp.boot.seq]
eq_homgl [prf, in mathcomp.finite_group.morphism]
eq_homgr [prf, in mathcomp.finite_group.morphism]
eq_homGrp [prf, in mathcomp.finite_group.presentation]
eq_image [prf, in mathcomp.boot.fintype]
eq_imset [prf, in mathcomp.boot.finset]
eq_in_all [prf, in mathcomp.boot.seq]
eq_in_allpairs [prf, in mathcomp.boot.seq]
eq_in_allpairs_dep [prf, in mathcomp.boot.seq]
eq_in_allrel [prf, in mathcomp.boot.seq]
eq_in_count [prf, in mathcomp.boot.seq]
eq_in_cycle [prf, in mathcomp.boot.path]
eq_in_filter [prf, in mathcomp.boot.seq]
eq_in_find [prf, in mathcomp.boot.seq]
eq_in_has [prf, in mathcomp.boot.seq]
eq_in_imset [prf, in mathcomp.boot.finset]
eq_in_imset2 [prf, in mathcomp.boot.finset]
eq_in_limg [prf, in mathcomp.algebra.vector]
eq_in_map [prf, in mathcomp.boot.seq]
eq_in_map2_mx [prf, in mathcomp.algebra.matrix]
eq_in_map_mx [prf, in mathcomp.algebra.matrix]
eq_in_map_poly [prf, in mathcomp.algebra.poly]
eq_in_map_poly_id0 [prf, in mathcomp.algebra.poly]
eq_in_morphim [prf, in mathcomp.finite_group.morphism]
eq_in_pairwise [prf, in mathcomp.boot.seq]
eq_in_partn [prf, in mathcomp.boot.prime]
eq_in_path [prf, in mathcomp.boot.path]
eq_in_pcore [prf, in mathcomp.solvable.pgroup]
eq_in_pHall [prf, in mathcomp.solvable.pgroup]
eq_in_pmap [prf, in mathcomp.boot.seq]
eq_in_pnat [prf, in mathcomp.boot.prime]
eq_in_sorted [prf, in mathcomp.boot.path]
eq_injectiveb [prf, in mathcomp.boot.fintype]
eq_invF [prf, in mathcomp.boot.fintype]
eq_invg1 [abbrev, in mathcomp.finite_group.fingroup]
eq_invg_mul [prf, in mathcomp.finite_group.fingroup]
eq_invg_sym [abbrev, in mathcomp.finite_group.fingroup]
eq_irr_mem_classP [prf, in mathcomp.group_representation.character]
eq_irrelevance [prf, in mathcomp.boot.eqtype]
eq_iter [prf, in mathcomp.boot.ssrnat]
eq_iteri [prf, in mathcomp.boot.ssrnat]
eq_iterop [prf, in mathcomp.boot.ssrnat]
eq_leq [prf, in mathcomp.boot.ssrnat]
eq_leqif [prf, in mathcomp.boot.ssrnat]
eq_liftF [prf, in mathcomp.boot.fintype]
eq_limg_ker0 [prf, in mathcomp.algebra.vector]
eq_lock [prf, in mathcomp.boot.generic_quotient]
eq_lrshift [prf, in mathcomp.boot.fintype]
eq_lshift [prf, in mathcomp.boot.fintype]
eq_map [prf, in mathcomp.boot.seq]
eq_map2_mx [prf, in mathcomp.algebra.matrix]
eq_map_all [prf, in mathcomp.boot.seq]
eq_map_mx [prf, in mathcomp.algebra.matrix]
eq_map_mx_id [prf, in mathcomp.algebra.sesquilinear]
eq_map_poly [prf, in mathcomp.algebra.poly]
eq_maxrowsub [prf, in mathcomp.algebra.mxalgebra]
eq_mem_map [prf, in mathcomp.boot.seq]
eq_mkseq [prf, in mathcomp.boot.seq]
eq_mktuple [prf, in mathcomp.boot.tuple]
eq_Mod8_D8 [prf, in mathcomp.solvable.extremal]
eq_morphim [prf, in mathcomp.finite_group.morphism]
eq_mul_cfuni [prf, in mathcomp.group_representation.classfun]
eq_mulgV1 [prf, in mathcomp.finite_group.fingroup]
eq_mulVg1 [prf, in mathcomp.finite_group.fingroup]
eq_mx [prf, in mathcomp.algebra.matrix]
eq_mxblock [prf, in mathcomp.algebra.matrix]
eq_mxblockP [prf, in mathcomp.algebra.matrix]
eq_mxcol [prf, in mathcomp.algebra.matrix]
eq_mxcolP [prf, in mathcomp.algebra.matrix]
eq_mxdiag [prf, in mathcomp.algebra.matrix]
eq_mxdiagP [prf, in mathcomp.algebra.matrix]
eq_mxrow [prf, in mathcomp.algebra.matrix]
eq_mxrowP [prf, in mathcomp.algebra.matrix]
eq_mxsub [prf, in mathcomp.algebra.matrix]
eq_n_comp [prf, in mathcomp.boot.fingraph]
eq_n_comp_r [prf, in mathcomp.boot.fingraph]
eq_negn [prf, in mathcomp.boot.prime]
eq_omap [prf, in mathcomp.boot.ssrfun]
eq_onthP [prf, in mathcomp.boot.seq]
eq_op [def, in mathcomp.boot.eqtype]
eq_op_trans [prf, in mathcomp.boot.generic_quotient]
eq_order_cycle [prf, in mathcomp.boot.fingraph]
eq_orthogonal [prf, in mathcomp.group_representation.classfun]
eq_orthonormal [prf, in mathcomp.group_representation.classfun]
eq_orthonormal [prf, in mathcomp.algebra.sesquilinear]
eq_p'core [prf, in mathcomp.solvable.pgroup]
eq_p'group [prf, in mathcomp.solvable.pgroup]
eq_p'Hall [prf, in mathcomp.solvable.pgroup]
eq_p_elt [prf, in mathcomp.solvable.pgroup]
eq_pairwise [prf, in mathcomp.boot.seq]
eq_pairwise_orthogonal [prf, in mathcomp.group_representation.classfun]
eq_pairwise_orthogonal [prf, in mathcomp.algebra.sesquilinear]
eq_partn [prf, in mathcomp.boot.prime]
eq_partn_from_log [prf, in mathcomp.boot.prime]
eq_path [prf, in mathcomp.boot.path]
eq_pblock [prf, in mathcomp.boot.finset]
eq_pcore [prf, in mathcomp.solvable.pgroup]
eq_pgroup [prf, in mathcomp.solvable.pgroup]
eq_pHall [prf, in mathcomp.solvable.pgroup]
eq_pick [prf, in mathcomp.boot.fintype]
eq_piP [prf, in mathcomp.boot.prime]
eq_pmap [prf, in mathcomp.boot.seq]
eq_pnat [prf, in mathcomp.boot.prime]
eq_poly [prf, in mathcomp.algebra.poly]
eq_porbit_mem [prf, in mathcomp.finite_group.perm]
eq_preimset [prf, in mathcomp.boot.finset]
eq_prim_root_expr [prf, in mathcomp.algebra.poly]
eq_primes [prf, in mathcomp.boot.prime]
eq_proper [prf, in mathcomp.boot.fintype]
eq_proper_r [prf, in mathcomp.boot.fintype]
eq_rank_unitmx [prf, in mathcomp.algebra.mxalgebra]
eq_refl [prf, in mathcomp.boot.eqtype]
eq_rlshift [prf, in mathcomp.boot.fintype]
eq_root [prf, in mathcomp.boot.fingraph]
eq_roots [prf, in mathcomp.boot.fingraph]
eq_row_base [prf, in mathcomp.algebra.mxalgebra]
eq_row_full [prf, in mathcomp.algebra.mxalgebra]
eq_row_mx [prf, in mathcomp.algebra.matrix]
eq_row_sub [prf, in mathcomp.algebra.mxalgebra]
eq_rowg [prf, in mathcomp.group_representation.mxabelem]
eq_rowsub [prf, in mathcomp.algebra.matrix]
eq_rshift [prf, in mathcomp.boot.fintype]
eq_scale_irr [prf, in mathcomp.group_representation.character]
eq_scaled_irr [prf, in mathcomp.group_representation.character]
eq_setXn [prf, in mathcomp.boot.finset]
eq_shift [def, in mathcomp.boot.fintype]
eq_signed_irr [prf, in mathcomp.group_representation.character]
eq_sorted [prf, in mathcomp.boot.path]
eq_span [prf, in mathcomp.algebra.vector]
eq_subG_cyclic [prf, in mathcomp.solvable.cyclic]
eq_subset [prf, in mathcomp.boot.fintype]
eq_subset_r [prf, in mathcomp.boot.fintype]
eq_subxx [prf, in mathcomp.boot.fintype]
eq_subZnat_irr [prf, in mathcomp.group_representation.character]
eq_sum_nth_irr [prf, in mathcomp.group_representation.character]
eq_sym [prf, in mathcomp.boot.eqtype]
eq_tag [prf, in mathcomp.boot.eqtype]
eq_Tagged [prf, in mathcomp.boot.eqtype]
eq_uniq [prf, in mathcomp.boot.seq]
eq_xchoose [prf, in mathcomp.boot.choice]
eq_xor_neq [ind, in mathcomp.boot.eqtype]
eqAmod [def, in mathcomp.field.algnum]
eqAmod0 [prf, in mathcomp.field.algnum]
eqAmod0_nat [prf, in mathcomp.field.algnum]
eqAmod0_rat [prf, in mathcomp.field.algnum]
eqAmod_addl_mul [prf, in mathcomp.field.algnum]
eqAmod_nat [prf, in mathcomp.field.algnum]
eqAmod_rat [prf, in mathcomp.field.algnum]
eqAmod_refl [prf, in mathcomp.field.algnum]
eqAmod_sym [prf, in mathcomp.field.algnum]
eqAmod_trans [prf, in mathcomp.field.algnum]
eqAmod_transl [prf, in mathcomp.field.algnum]
eqAmod_transr [prf, in mathcomp.field.algnum]
eqAmodD [prf, in mathcomp.field.algnum]
eqAmodDl [prf, in mathcomp.field.algnum]
eqAmodDr [prf, in mathcomp.field.algnum]
eqAmodM [prf, in mathcomp.field.algnum]
eqAmodm0 [prf, in mathcomp.field.algnum]
eqAmodMl [prf, in mathcomp.field.algnum]
eqAmodMl0 [prf, in mathcomp.field.algnum]
eqAmodMr [prf, in mathcomp.field.algnum]
eqAmodMr0 [prf, in mathcomp.field.algnum]
eqAmodN [prf, in mathcomp.field.algnum]
eqb [def, in mathcomp.boot.eqtype]
eqb0 [prf, in mathcomp.boot.ssrnat]
eqb1 [prf, in mathcomp.boot.ssrnat]
eqb_id [prf, in mathcomp.boot.eqtype]
eqb_negLR [prf, in mathcomp.boot.eqtype]
eqbE [prf, in mathcomp.boot.eqtype]
eqbF_neg [prf, in mathcomp.boot.eqtype]
eqbLHS [abbrev, in mathcomp.boot.eqtype]
eqbP [prf, in mathcomp.boot.eqtype]
eqbRHS [abbrev, in mathcomp.boot.eqtype]
eqC_nat [def, in mathcomp.field.algC]
eqcfP [abbrev, in mathcomp.group_representation.classfun]
eqCmod0 [prf, in mathcomp.field.algC]
eqCmod0_nat [prf, in mathcomp.field.algC]
eqCmod_addl_mul [prf, in mathcomp.field.algC]
eqCmod_nat [prf, in mathcomp.field.algC]
eqCmod_refl [prf, in mathcomp.field.algC]
eqCmod_sym [prf, in mathcomp.field.algC]
eqCmod_trans [prf, in mathcomp.field.algC]
eqCmod_transl [prf, in mathcomp.field.algC]
eqCmod_transr [prf, in mathcomp.field.algC]
eqCmodD [prf, in mathcomp.field.algC]
eqCmodDl [prf, in mathcomp.field.algC]
eqCmodDr [prf, in mathcomp.field.algC]
eqCmodM [prf, in mathcomp.field.algC]
eqCmodm0 [prf, in mathcomp.field.algC]
eqCmodMl [prf, in mathcomp.field.algC]
eqCmodMl0 [prf, in mathcomp.field.algC]
eqCmodMr [prf, in mathcomp.field.algC]
eqCmodMr0 [prf, in mathcomp.field.algC]
eqCmodN [prf, in mathcomp.field.algC]
eqE [prf, in mathcomp.boot.eqtype]
eqEcard [prf, in mathcomp.boot.finset]
eqEdim [prf, in mathcomp.algebra.vector]
eqEproper [prf, in mathcomp.boot.finset]
eqEsubset [prf, in mathcomp.boot.finset]
eqEsubv [prf, in mathcomp.algebra.vector]
eqEtuple [prf, in mathcomp.boot.tuple]
eqfun_inP [prf, in mathcomp.boot.fintype]
eqfunP [prf, in mathcomp.boot.fintype]
eqg_inv [prf, in mathcomp.boot.monoid]
eqg_invLR [prf, in mathcomp.boot.monoid]
eqg_mx_abs_irr [prf, in mathcomp.group_representation.mxrepresentation]
eqg_mx_faithful [prf, in mathcomp.group_representation.mxrepresentation]
eqg_mx_irr [prf, in mathcomp.group_representation.mxrepresentation]
eqg_repr [def, in mathcomp.group_representation.mxrepresentation]
eqg_repr_proof [prf, in mathcomp.group_representation.mxrepresentation]
eqlfun_inP [prf, in mathcomp.algebra.vector]
eqlfunP [prf, in mathcomp.algebra.vector]
eqmodE [prf, in mathcomp.boot.generic_quotient]
eqmodP [prf, in mathcomp.boot.generic_quotient]
eqmx [def, in mathcomp.algebra.mxalgebra]
eqmx0 [prf, in mathcomp.algebra.mxalgebra]
eqmx0P [prf, in mathcomp.algebra.mxalgebra]
eqmx_cast [prf, in mathcomp.algebra.mxalgebra]
eqmx_col [prf, in mathcomp.algebra.mxalgebra]
eqmx_conform [prf, in mathcomp.algebra.mxalgebra]
eqmx_eq0 [prf, in mathcomp.algebra.mxalgebra]
eqmx_iso [prf, in mathcomp.group_representation.mxrepresentation]
eqmx_module [prf, in mathcomp.group_representation.mxrepresentation]
eqmx_opp [prf, in mathcomp.algebra.mxalgebra]
eqmx_ortho [prf, in mathcomp.algebra.sesquilinear]
eqmx_rank [prf, in mathcomp.algebra.mxalgebra]
eqmx_refl [prf, in mathcomp.algebra.mxalgebra]
eqmx_ReiIm [prf, in mathcomp.algebra.spectral]
eqmx_rowsub [prf, in mathcomp.algebra.mxalgebra]
eqmx_rowsub_comp [prf, in mathcomp.algebra.mxalgebra]
eqmx_rowsub_comp_perm [prf, in mathcomp.algebra.mxalgebra]
eqmx_rstab [prf, in mathcomp.group_representation.mxrepresentation]
eqmx_rstabs [prf, in mathcomp.group_representation.mxrepresentation]
eqmx_scale [prf, in mathcomp.algebra.mxalgebra]
eqmx_schmidt_free [prf, in mathcomp.algebra.spectral]
eqmx_schmidt_full [prf, in mathcomp.algebra.spectral]
eqmx_semisimple [prf, in mathcomp.group_representation.mxrepresentation]
eqmx_stable [prf, in mathcomp.algebra.mxalgebra]
eqmx_sums [prf, in mathcomp.algebra.mxalgebra]
eqmx_sym [prf, in mathcomp.algebra.mxalgebra]
eqmx_trans [prf, in mathcomp.algebra.mxalgebra]
eqmxMfree [prf, in mathcomp.algebra.mxalgebra]
eqmxMfull [prf, in mathcomp.algebra.mxalgebra]
eqmxMr [prf, in mathcomp.algebra.mxalgebra]
eqmxMunitP [prf, in mathcomp.algebra.mxalgebra]
eqmxP [prf, in mathcomp.algebra.mxalgebra]
eqn [def, in mathcomp.boot.ssrnat]
eqn0_xor_gt0 [ind, in mathcomp.boot.ssrnat]
eqn0F [prf, in mathcomp.algebra.interval_inference]
eqn0Ngt [prf, in mathcomp.boot.ssrnat]
eqn_add2l [prf, in mathcomp.boot.ssrnat]
eqn_add2r [prf, in mathcomp.boot.ssrnat]
eqn_div [prf, in mathcomp.boot.div]
eqn_dvd [prf, in mathcomp.boot.div]
eqn_exp2l [prf, in mathcomp.boot.ssrnat]
eqn_exp2r [prf, in mathcomp.boot.ssrnat]
eqn_from_log [prf, in mathcomp.boot.prime]
eqn_geP [prf, in mathcomp.boot.ssrnat]
eqn_gtP [prf, in mathcomp.boot.ssrnat]
eqn_leP [prf, in mathcomp.boot.ssrnat]
eqn_leq [prf, in mathcomp.boot.ssrnat]
eqn_ltP [prf, in mathcomp.boot.ssrnat]
eqn_mod_dvd [prf, in mathcomp.boot.div]
eqn_modDl [prf, in mathcomp.boot.div]
eqn_modDr [prf, in mathcomp.boot.div]
eqn_mul [prf, in mathcomp.boot.div]
eqn_mul2l [prf, in mathcomp.boot.ssrnat]
eqn_mul2r [prf, in mathcomp.boot.ssrnat]
eqn_pmul2l [prf, in mathcomp.boot.ssrnat]
eqn_pmul2r [prf, in mathcomp.boot.ssrnat]
eqn_sqr [prf, in mathcomp.boot.ssrnat]
eqn_sub2lE [prf, in mathcomp.boot.ssrnat]
eqn_sub2rE [prf, in mathcomp.boot.ssrnat]
eqnE [prf, in mathcomp.boot.ssrnat]
EqNotNeq [constr, in mathcomp.boot.eqtype]
eqnP [prf, in mathcomp.boot.ssrnat]
eqP [def, in mathcomp.boot.eqtype]
eqp_separable [prf, in mathcomp.field.separable]
eqp_take_drop [prf, in mathcomp.algebra.poly]
eqperm [prf, in mathcomp.solvable.burnside_app]
eqperm_map [prf, in mathcomp.solvable.burnside_app]
eqperm_map2 [prf, in mathcomp.solvable.burnside_app]
eqquotE [prf, in mathcomp.boot.generic_quotient]
EqQuotient [abbrev, in mathcomp.boot.generic_quotient]
EqQuotient [mod, in mathcomp.boot.generic_quotient]
EqQuotient.axioms_ [rec, in mathcomp.boot.generic_quotient]
EqQuotient.class [proj, in mathcomp.boot.generic_quotient]
EqQuotient.clone [abbrev, in mathcomp.boot.generic_quotient]
EqQuotient.copy [abbrev, in mathcomp.boot.generic_quotient]
EqQuotient.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.generic_quotient]
EqQuotient.Exports [mod, in mathcomp.boot.generic_quotient]
EqQuotient.Exports.eqQuotType [abbrev, in mathcomp.boot.generic_quotient]
EqQuotient.Exports.join_generic_quotient_EqQuotient_between_eqtype_Equality_and_generic_quotient_Quotient [def, in mathcomp.boot.generic_quotient]
EqQuotient.generic_quotient_isEqQuotient_mixin [proj, in mathcomp.boot.generic_quotient]
EqQuotient.generic_quotient_isQuotient_mixin [proj, in mathcomp.boot.generic_quotient]
EqQuotient.on [abbrev, in mathcomp.boot.generic_quotient]
EqQuotient.on_ [abbrev, in mathcomp.boot.generic_quotient]
EqQuotient.pack_ [def, in mathcomp.boot.generic_quotient]
EqQuotient.phant_clone [def, in mathcomp.boot.generic_quotient]
EqQuotient.phant_on_ [def, in mathcomp.boot.generic_quotient]
EqQuotient.sort [proj, in mathcomp.boot.generic_quotient]
EqQuotient.type [rec, in mathcomp.boot.generic_quotient]
EqQuotientElpiOperations [mod, in mathcomp.boot.generic_quotient]
eqquotP [prf, in mathcomp.boot.generic_quotient]
eqr_int [prf, in mathcomp.algebra.ssrint]
eqrXz2 [prf, in mathcomp.algebra.ssrint]
eqseq [def, in mathcomp.boot.seq]
eqseq_all [prf, in mathcomp.boot.seq]
eqseq_cat [prf, in mathcomp.boot.seq]
eqseq_cons [prf, in mathcomp.boot.seq]
eqseq_pivot2l [prf, in mathcomp.boot.seq]
eqseq_pivot2r [prf, in mathcomp.boot.seq]
eqseq_pivotl [prf, in mathcomp.boot.seq]
eqseq_pivotr [prf, in mathcomp.boot.seq]
eqseq_rcons [prf, in mathcomp.boot.seq]
eqseq_rot [prf, in mathcomp.boot.seq]
eqseqE [prf, in mathcomp.boot.seq]
eqseqP [prf, in mathcomp.boot.seq]
eqSS [prf, in mathcomp.boot.ssrnat]
eqsVneq [prf, in mathcomp.boot.finset]
eqTleqif [prf, in mathcomp.boot.ssrnat]
eqtype [file, in mathcomp.boot.eqtype]
EqTypePred [mod, in mathcomp.boot.eqtype]
EqTypePredSig [modtype, in mathcomp.boot.eqtype]
EqTypePredSig.sort [ax, in mathcomp.boot.eqtype]
equal_to [rec, in mathcomp.boot.generic_quotient]
equal_to_pi [def, in mathcomp.boot.generic_quotient]
equal_toE [prf, in mathcomp.boot.generic_quotient]
equal_val [proj, in mathcomp.boot.generic_quotient]
Equality [abbrev, in mathcomp.boot.eqtype]
Equality [mod, in mathcomp.boot.eqtype]
Equality.axioms_ [rec, in mathcomp.boot.eqtype]
Equality.class [proj, in mathcomp.boot.eqtype]
Equality.clone [abbrev, in mathcomp.boot.eqtype]
Equality.copy [abbrev, in mathcomp.boot.eqtype]
Equality.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.eqtype]
Equality.Exports [mod, in mathcomp.boot.eqtype]
Equality.Exports.eqType [abbrev, in mathcomp.boot.eqtype]
Equality.on [abbrev, in mathcomp.boot.eqtype]
Equality.on_ [abbrev, in mathcomp.boot.eqtype]
Equality.pack_ [def, in mathcomp.boot.eqtype]
Equality.phant_clone [def, in mathcomp.boot.eqtype]
Equality.phant_on_ [def, in mathcomp.boot.eqtype]
Equality.sort [proj, in mathcomp.boot.eqtype]
Equality.type [rec, in mathcomp.boot.eqtype]
EqualityElpiOperations [mod, in mathcomp.boot.eqtype]
equiv [proj, in mathcomp.boot.generic_quotient]
equiv_class [def, in mathcomp.boot.generic_quotient]
equiv_class_of [ind, in mathcomp.boot.generic_quotient]
equiv_ltrans [prf, in mathcomp.boot.generic_quotient]
equiv_pack [def, in mathcomp.boot.generic_quotient]
equiv_refl [prf, in mathcomp.boot.generic_quotient]
equiv_rel [rec, in mathcomp.boot.generic_quotient]
equiv_rtrans [prf, in mathcomp.boot.generic_quotient]
equiv_subfext [def, in mathcomp.field.fieldext]
equiv_subfext_encModRel [def, in mathcomp.field.fieldext]
equiv_subfext_equiv [def, in mathcomp.field.fieldext]
equiv_subfext_is_equiv [prf, in mathcomp.field.fieldext]
equiv_sym [prf, in mathcomp.boot.generic_quotient]
equiv_trans [prf, in mathcomp.boot.generic_quotient]
equivalence_partition [def, in mathcomp.boot.finset]
equivalence_partition_pblock [prf, in mathcomp.boot.finset]
equivalence_partitionP [prf, in mathcomp.boot.finset]
EquivClass [constr, in mathcomp.boot.generic_quotient]
equivf [abbrev, in mathcomp.algebra.fraction]
equivmx [def, in mathcomp.algebra.mxalgebra]
equivmx_spec [def, in mathcomp.algebra.mxalgebra]
EquivQuot [mod, in mathcomp.boot.generic_quotient]
EquivQuot.canon [def, in mathcomp.boot.generic_quotient]
EquivQuot.canon_id [prf, in mathcomp.boot.generic_quotient]
EquivQuot.eC [abbrev, in mathcomp.boot.generic_quotient]
EquivQuot.encD_equiv_rel [def, in mathcomp.boot.generic_quotient]
EquivQuot.encDE [abbrev, in mathcomp.boot.generic_quotient]
EquivQuot.encDP [abbrev, in mathcomp.boot.generic_quotient]
EquivQuot.eqmodE [prf, in mathcomp.boot.generic_quotient]
EquivQuot.eqmodP [prf, in mathcomp.boot.generic_quotient]
EquivQuot.equivQTP [prf, in mathcomp.boot.generic_quotient]
EquivQuot.equivQuotient [rec, in mathcomp.boot.generic_quotient]
EquivQuot.erepr [proj, in mathcomp.boot.generic_quotient]
EquivQuot.ereprK [prf, in mathcomp.boot.generic_quotient]
EquivQuot.Exports [mod, in mathcomp.boot.generic_quotient]
EquivQuot.pi [def, in mathcomp.boot.generic_quotient]
EquivQuot.pi_CD [prf, in mathcomp.boot.generic_quotient]
EquivQuot.pi_DC [prf, in mathcomp.boot.generic_quotient]
EquivQuot.qT [abbrev, in mathcomp.boot.generic_quotient]
EquivQuot.type_of [def, in mathcomp.boot.generic_quotient]
EquivRel [abbrev, in mathcomp.boot.generic_quotient]
eqVneq [prf, in mathcomp.boot.eqtype]
eqVproper [prf, in mathcomp.boot.finset]
eqxx [abbrev, in mathcomp.boot.eqtype]
eqz_div [prf, in mathcomp.algebra.intdiv]
eqz_mod_dvd [prf, in mathcomp.algebra.intdiv]
eqz_modDl [prf, in mathcomp.algebra.intdiv]
eqz_modDr [prf, in mathcomp.algebra.intdiv]
eqz_mul [prf, in mathcomp.algebra.intdiv]
eqz_nat [prf, in mathcomp.algebra.ssrint]
ErV [abbrev, in mathcomp.group_representation.mxabelem]
etagged [def, in mathcomp.boot.eqtype]
etaggedE [prf, in mathcomp.boot.finfun]
etaggedK [prf, in mathcomp.boot.eqtype]
Euclid_dvd1 [prf, in mathcomp.boot.prime]
Euclid_dvd_prod [prf, in mathcomp.boot.prime]
Euclid_dvdM [prf, in mathcomp.boot.prime]
Euclid_dvdX [prf, in mathcomp.boot.prime]
Euler_exp_totient [prf, in mathcomp.solvable.cyclic]
ev_ax [abbrev, in mathcomp.boot.eqtype]
eval [abbrev, in mathcomp.group_representation.mxrepresentation]
eval [abbrev, in mathcomp.algebra.polyXY]
eval_mxmodule [prf, in mathcomp.group_representation.mxrepresentation]
even_halfK [prf, in mathcomp.boot.ssrnat]
even_poly [def, in mathcomp.algebra.poly]
even_poly_is_linear [prf, in mathcomp.algebra.poly]
even_polyC [prf, in mathcomp.algebra.poly]
even_polyD [prf, in mathcomp.algebra.poly]
even_polyE [prf, in mathcomp.algebra.poly]
even_polyMX [prf, in mathcomp.algebra.poly]
even_polyZ [prf, in mathcomp.algebra.poly]
even_prime [prf, in mathcomp.boot.prime]
even_uphalfK [prf, in mathcomp.boot.ssrnat]
ex_maxgroup [prf, in mathcomp.finite_group.fingroup]
ex_maxn [def, in mathcomp.boot.ssrnat]
ex_maxn_spec [ind, in mathcomp.boot.ssrnat]
ex_maxnormal_ntrivg [prf, in mathcomp.solvable.gseries]
ex_maxnP [prf, in mathcomp.boot.ssrnat]
ex_maxset [prf, in mathcomp.boot.finset]
ex_mingroup [prf, in mathcomp.finite_group.fingroup]
ex_minn [def, in mathcomp.boot.ssrnat]
ex_minn_spec [ind, in mathcomp.boot.ssrnat]
ex_minn_spec_ind [scheme, in mathcomp.boot.ssrnat]
ex_minn_spec_rec [scheme, in mathcomp.boot.ssrnat]
ex_minn_spec_rect [scheme, in mathcomp.boot.ssrnat]
ex_minn_spec_sind [scheme, in mathcomp.boot.ssrnat]
ex_minnP [prf, in mathcomp.boot.ssrnat]
ex_minset [prf, in mathcomp.boot.finset]
exchange_big [prf, in mathcomp.boot.bigop]
exchange_big_dep [prf, in mathcomp.boot.bigop]
exchange_big_dep_idem [prf, in mathcomp.boot.bigop]
exchange_big_dep_nat [prf, in mathcomp.boot.bigop]
exchange_big_dep_nat_idem [prf, in mathcomp.boot.bigop]
exchange_big_idem [prf, in mathcomp.boot.bigop]
exchange_big_nat [prf, in mathcomp.boot.bigop]
exchange_big_nat_idem [prf, in mathcomp.boot.bigop]
exists_acomps [prf, in mathcomp.solvable.jordanholder]
exists_comps [prf, in mathcomp.solvable.jordanholder]
exists_cons [prf, in mathcomp.boot.seq]
exists_eq_inP [prf, in mathcomp.boot.fintype]
exists_eqP [prf, in mathcomp.boot.fintype]
exists_inb [prf, in mathcomp.boot.fintype]
exists_inP [prf, in mathcomp.boot.fintype]
exists_inPn [prf, in mathcomp.boot.fintype]
exists_inPP [prf, in mathcomp.boot.fintype]
existsb [prf, in mathcomp.boot.fintype]
existsb_tnth [prf, in mathcomp.boot.tuple]
existsbWl [prf, in mathcomp.boot.fintype]
existsbWr [prf, in mathcomp.boot.fintype]
existsP [prf, in mathcomp.boot.fintype]
existsPn [prf, in mathcomp.boot.fintype]
existsPP [prf, in mathcomp.boot.fintype]
ExMaxnSpec [constr, in mathcomp.boot.ssrnat]
ExMinnSpec [constr, in mathcomp.boot.ssrnat]
exp0n [prf, in mathcomp.boot.ssrnat]
exp0rz [prf, in mathcomp.algebra.ssrint]
exp1n [prf, in mathcomp.boot.ssrnat]
exp1rz [prf, in mathcomp.algebra.ssrint]
exp_block_diag_mx [prf, in mathcomp.algebra.matrix]
exp_cforder [prf, in mathcomp.group_representation.classfun]
exp_cfunE [prf, in mathcomp.group_representation.classfun]
exp_finIndexType [def, in mathcomp.boot.finfun]
exp_orderC [prf, in mathcomp.field.algnum]
exp_prim_root [prf, in mathcomp.algebra.poly]
expand_cofactor [prf, in mathcomp.algebra.matrix]
expand_det_col [prf, in mathcomp.algebra.matrix]
expand_det_row [prf, in mathcomp.algebra.matrix]
expf_card [prf, in mathcomp.field.finfield]
expfV [prf, in mathcomp.algebra.ssrint]
expfz_eq0 [prf, in mathcomp.algebra.ssrint]
expfz_n0addr [prf, in mathcomp.algebra.ssrint]
expfz_neq0 [prf, in mathcomp.algebra.ssrint]
expfzDr [prf, in mathcomp.algebra.ssrint]
expfzMl [prf, in mathcomp.algebra.ssrint]
expg0 [abbrev, in mathcomp.finite_group.fingroup]
expg0 [prf, in mathcomp.boot.monoid]
expg1 [abbrev, in mathcomp.finite_group.fingroup]
expg1 [prf, in mathcomp.boot.monoid]
expg1n [abbrev, in mathcomp.finite_group.fingroup]
expg1n [prf, in mathcomp.boot.monoid]
expg2 [prf, in mathcomp.boot.monoid]
expg_cardG [prf, in mathcomp.solvable.cyclic]
expg_exponent [prf, in mathcomp.solvable.abelian]
expg_invn [def, in mathcomp.solvable.cyclic]
expg_mod [prf, in mathcomp.finite_group.fingroup]
expg_mod_order [prf, in mathcomp.finite_group.fingroup]
expg_order [prf, in mathcomp.finite_group.fingroup]
expg_znat [prf, in mathcomp.solvable.cyclic]
expg_zneg [prf, in mathcomp.solvable.cyclic]
expgAC [abbrev, in mathcomp.finite_group.fingroup]
expgb [prf, in mathcomp.boot.monoid]
expgD [abbrev, in mathcomp.finite_group.fingroup]
expgD_Zp [prf, in mathcomp.solvable.cyclic]
expgK [prf, in mathcomp.solvable.cyclic]
expgM [abbrev, in mathcomp.finite_group.fingroup]
expgMn [abbrev, in mathcomp.finite_group.fingroup]
expgMn [prf, in mathcomp.boot.monoid]
expgn [abbrev, in mathcomp.finite_group.fingroup]
expgnA [prf, in mathcomp.boot.monoid]
expgnAC [prf, in mathcomp.boot.monoid]
expgnDr [prf, in mathcomp.boot.monoid]
expgnE [abbrev, in mathcomp.finite_group.fingroup]
expgnE [prf, in mathcomp.boot.monoid]
expgnFl [prf, in mathcomp.boot.monoid]
expgnFr [prf, in mathcomp.boot.monoid]
expgS [prf, in mathcomp.boot.monoid]
expgSr [abbrev, in mathcomp.finite_group.fingroup]
expgSr [prf, in mathcomp.boot.monoid]
expgSS [prf, in mathcomp.boot.monoid]
expgVn [abbrev, in mathcomp.finite_group.fingroup]
expIn [prf, in mathcomp.boot.ssrnat]
expMg_Rmul [prf, in mathcomp.solvable.commutator]
expn [def, in mathcomp.boot.ssrnat]
expn0 [prf, in mathcomp.boot.ssrnat]
expn1 [prf, in mathcomp.boot.ssrnat]
expN1r [prf, in mathcomp.algebra.ssrint]
expn_eq0 [prf, in mathcomp.boot.ssrnat]
expn_gt0 [prf, in mathcomp.boot.ssrnat]
expn_max [prf, in mathcomp.boot.div]
expn_min [prf, in mathcomp.boot.div]
expn_rec [def, in mathcomp.boot.ssrnat]
expn_sum [prf, in mathcomp.boot.bigop]
expnAC [prf, in mathcomp.boot.ssrnat]
expnB [prf, in mathcomp.boot.div]
expnD [prf, in mathcomp.boot.ssrnat]
expnDn [prf, in mathcomp.boot.binomial]
expnE [prf, in mathcomp.boot.ssrnat]
expnI [prf, in mathcomp.boot.ssrnat]
expnM [prf, in mathcomp.boot.ssrnat]
expnMn [prf, in mathcomp.boot.ssrnat]
expNrz [prf, in mathcomp.algebra.ssrint]
expnS [prf, in mathcomp.boot.ssrnat]
expnSr [prf, in mathcomp.boot.ssrnat]
exponent [def, in mathcomp.solvable.abelian]
exponent1 [prf, in mathcomp.solvable.abelian]
exponent2_abelem [prf, in mathcomp.solvable.abelian]
exponent_2extraspecial [prf, in mathcomp.solvable.maximal]
exponent_cycle [prf, in mathcomp.solvable.abelian]
exponent_cyclic [prf, in mathcomp.solvable.abelian]
exponent_dprod_homocyclic [prf, in mathcomp.solvable.abelian]
exponent_dvdn [prf, in mathcomp.solvable.abelian]
exponent_gt0 [prf, in mathcomp.solvable.abelian]
exponent_Hall [prf, in mathcomp.solvable.abelian]
exponent_injm [prf, in mathcomp.solvable.abelian]
exponent_isog [prf, in mathcomp.solvable.abelian]
exponent_morphim [prf, in mathcomp.solvable.abelian]
exponent_mx_group [prf, in mathcomp.group_representation.mxabelem]
exponent_Ohm1_class2 [prf, in mathcomp.solvable.maximal]
exponent_pX1p2 [prf, in mathcomp.solvable.extraspecial]
exponent_pX1p2n [prf, in mathcomp.solvable.extraspecial]
exponent_quotient [prf, in mathcomp.solvable.abelian]
exponent_special [prf, in mathcomp.solvable.maximal]
exponent_witness [prf, in mathcomp.solvable.abelian]
exponent_Zgroup [prf, in mathcomp.solvable.abelian]
exponentJ [prf, in mathcomp.solvable.abelian]
exponentP [prf, in mathcomp.solvable.abelian]
exponentS [prf, in mathcomp.solvable.abelian]
expr0z [prf, in mathcomp.algebra.ssrint]
expr1z [prf, in mathcomp.algebra.ssrint]
exprMz_comm [prf, in mathcomp.algebra.ssrint]
exprN1 [prf, in mathcomp.algebra.ssrint]
exprnN [prf, in mathcomp.algebra.ssrint]
exprnP [prf, in mathcomp.algebra.ssrint]
exprSz [prf, in mathcomp.algebra.ssrint]
exprSzr [prf, in mathcomp.algebra.ssrint]
exprz [def, in mathcomp.algebra.ssrint]
exprz_exp [prf, in mathcomp.algebra.ssrint]
exprz_ge0 [prf, in mathcomp.algebra.ssrint]
exprz_gt0 [prf, in mathcomp.algebra.ssrint]
exprz_gte0 [def, in mathcomp.algebra.ssrint]
exprz_inv [prf, in mathcomp.algebra.ssrint]
exprz_out [prf, in mathcomp.algebra.ssrint]
exprz_pintl [prf, in mathcomp.algebra.ssrint]
exprz_pMzl [prf, in mathcomp.algebra.ssrint]
exprzAC [prf, in mathcomp.algebra.ssrint]
exprzD_nat [prf, in mathcomp.algebra.ssrint]
exprzD_Nnat [prf, in mathcomp.algebra.ssrint]
exprzD_ss [prf, in mathcomp.algebra.ssrint]
exprzDr [prf, in mathcomp.algebra.ssrint]
exprzMl [prf, in mathcomp.algebra.ssrint]
exprzMzl [prf, in mathcomp.algebra.ssrint]
expS_cfunE [prf, in mathcomp.group_representation.classfun]
expv [def, in mathcomp.field.falgebra]
expv0 [prf, in mathcomp.field.falgebra]
expv0n [prf, in mathcomp.field.falgebra]
expv1 [prf, in mathcomp.field.falgebra]
expv1n [prf, in mathcomp.field.falgebra]
expv2 [prf, in mathcomp.field.falgebra]
expv_id [prf, in mathcomp.field.falgebra]
expv_line [prf, in mathcomp.field.falgebra]
expvD [prf, in mathcomp.field.falgebra]
expVgn [prf, in mathcomp.boot.monoid]
expvM [prf, in mathcomp.field.falgebra]
expvS [prf, in mathcomp.field.falgebra]
expvSl [prf, in mathcomp.field.falgebra]
expvSr [prf, in mathcomp.field.falgebra]
expz_min [prf, in mathcomp.algebra.intdiv]
expzB [prf, in mathcomp.algebra.intdiv]
ext_coprime_Hall_exists [prf, in mathcomp.solvable.hall]
ext_coprime_Hall_subset [prf, in mathcomp.solvable.hall]
ext_coprime_Hall_trans [prf, in mathcomp.solvable.hall]
ext_coprime_quotient_cent [prf, in mathcomp.solvable.hall]
ext_norm_conj_cent [prf, in mathcomp.solvable.hall]
extend_algC_subfield_aut [prf, in mathcomp.field.algnum]
extend_cfConjC_subset [prf, in mathcomp.group_representation.classfun]
extend_coprime_linear_char [prf, in mathcomp.group_representation.inertia]
extend_cyclic_Mho [prf, in mathcomp.solvable.abelian]
extend_group_splitting_field [prf, in mathcomp.group_representation.mxrepresentation]
extend_linear_char_from_Sylow [prf, in mathcomp.group_representation.inertia]
extend_solvable_coprime_irr [prf, in mathcomp.group_representation.inertia]
extend_to_cfdet [prf, in mathcomp.group_representation.inertia]
extendDerivation [def, in mathcomp.field.separable]
extendDerivation_horner [prf, in mathcomp.field.separable]
extendDerivation_id [prf, in mathcomp.field.separable]
extendDerivationP [prf, in mathcomp.field.separable]
extendible_irr_invariant [prf, in mathcomp.group_representation.inertia]
external_action_im_coprime [prf, in mathcomp.solvable.hall]
extgK [abbrev, in mathcomp.solvable.extremal]
extnprod_invg [def, in mathcomp.finite_group.gproduct]
extnprod_mul1g [prf, in mathcomp.finite_group.gproduct]
extnprod_mulg [def, in mathcomp.finite_group.gproduct]
extnprod_mulgA [prf, in mathcomp.finite_group.gproduct]
extnprod_mulVg [prf, in mathcomp.finite_group.gproduct]
extprod_invg [def, in mathcomp.finite_group.gproduct]
extprod_mul1g [prf, in mathcomp.finite_group.gproduct]
extprod_mulg [def, in mathcomp.finite_group.gproduct]
extprod_mulgA [prf, in mathcomp.finite_group.gproduct]
extprod_mulVg [prf, in mathcomp.finite_group.gproduct]
extraspecial [file, in mathcomp.solvable.extraspecial]
extraspecial [def, in mathcomp.solvable.maximal]
extraspecial_nonabelian [prf, in mathcomp.solvable.maximal]
extraspecial_prime [prf, in mathcomp.solvable.maximal]
extraspecial_repr_structure [abbrev, in mathcomp.group_representation.mxabelem]
extraspecial_repr_structure_pchar [prf, in mathcomp.group_representation.mxabelem]
extraspecial_structure [prf, in mathcomp.solvable.maximal]
extremal [file, in mathcomp.solvable.extremal]
Extremal [mod, in mathcomp.solvable.extremal]
Extremal.act_dom [prf, in mathcomp.solvable.extremal]
Extremal.act_morphism [def, in mathcomp.solvable.extremal]
Extremal.aut_dvdn [prf, in mathcomp.solvable.extremal]
Extremal.aut_of [abbrev, in mathcomp.solvable.extremal]
Extremal.aut_of [def, in mathcomp.solvable.extremal]
Extremal.B [abbrev, in mathcomp.solvable.extremal]
Extremal.B [abbrev, in mathcomp.solvable.extremal]
Extremal.base_act [def, in mathcomp.solvable.extremal]
Extremal.card [prf, in mathcomp.solvable.extremal]
Extremal.gact [abbrev, in mathcomp.solvable.extremal]
Extremal.gact [def, in mathcomp.solvable.extremal]
Extremal.Grp [prf, in mathcomp.solvable.extremal]
Extremal.gtype [abbrev, in mathcomp.solvable.extremal]
Extremal.gtype [abbrev, in mathcomp.solvable.extremal]
Extremal.gtype [mod, in mathcomp.solvable.extremal]
Extremal.gtype.body [def, in mathcomp.solvable.extremal]
Extremal.gtype.unlock [def, in mathcomp.solvable.extremal]
Extremal.gtype_Locked [modtype, in mathcomp.solvable.extremal]
Extremal.gtype_Locked.body [ax, in mathcomp.solvable.extremal]
Extremal.gtype_Locked.unlock [ax, in mathcomp.solvable.extremal]
Extremal.gtype_unlock_subterm [def, in mathcomp.solvable.extremal]
Extremal.gtype_unlockable [def, in mathcomp.solvable.extremal]
extremal2 [def, in mathcomp.solvable.extremal]
extremal2_structure [prf, in mathcomp.solvable.extremal]
extremal_class [def, in mathcomp.solvable.extremal]
extremal_generators [def, in mathcomp.solvable.extremal]
extremal_generators_facts [prf, in mathcomp.solvable.extremal]
extremal_group_type [ind, in mathcomp.solvable.extremal]
extremal_group_type_ind [scheme, in mathcomp.solvable.extremal]
extremal_group_type_rec [scheme, in mathcomp.solvable.extremal]
extremal_group_type_rect [scheme, in mathcomp.solvable.extremal]
extremal_group_type_sind [scheme, in mathcomp.solvable.extremal]
extremum [def, in mathcomp.boot.fintype]
extremum_inP [prf, in mathcomp.boot.fintype]
extremum_spec [ind, in mathcomp.boot.fintype]
extremumP [prf, in mathcomp.boot.fintype]
ExtremumSpec [constr, in mathcomp.boot.fintype]