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 (14626 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 (165 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 (112 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 (7292 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 (761 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 (250 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 (390 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 (84 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 (3144 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 (126 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 (28 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 (2221 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 (53 entries)

E

ED [abbreviation, in extremal]
edivn [definition, in div]
edivnP [lemma, in div]
EdivnSpec [constructor, in poly]
EdivnSpec [constructor, in div]
edivn_spec [inductive, in div]
edivn_eq [lemma, in div]
edivn_rec [definition, in div]
edivn_def [lemma, in div]
edivn2 [definition, in prime]
edivn2P [lemma, in prime]
edivp [definition, in poly]
edivpP [lemma, in poly]
edivp_spec [inductive, in poly]
edivp_rec [definition, in poly]
edivp_map [lemma, in poly]
edivp_eq [lemma, in poly]
egcdn [definition, in div]
egcdnP [lemma, in div]
EgcdnSpec [constructor, in div]
egcdn_spec [inductive, in div]
egcdn_rec [definition, in div]
egcd0n [lemma, in div]
eigenspace [definition, in mxalgebra]
eigenspaceP [lemma, in mxalgebra]
eigenvalue [definition, in mxalgebra]
eigenvalueP [lemma, in mxalgebra]
eigenvalue_root_char [lemma, in mxpoly]
eigenvalue_root_min [lemma, in mxpoly]
eigenvalue_map [lemma, in mxalgebra]
ElementOps [section, in fingroup]
ElementOps.T [variable, in fingroup]
elimF [lemma, in ssrbool]
elimFn [lemma, in ssrbool]
elimN [lemma, in ssrbool]
elimNf [lemma, in ssrbool]
elimNTF [lemma, in ssrbool]
elimT [lemma, in ssrbool]
elimTF [lemma, in ssrbool]
elimTFn [lemma, in ssrbool]
elimTn [lemma, in ssrbool]
elogn2 [definition, in prime]
elogn2P [lemma, in prime]
Elogn2Spec [constructor, in prime]
elogn2_spec [inductive, in prime]
Eltm [section, in cyclic]
eltm [definition, in cyclic]
eltmE [lemma, in cyclic]
eltmM [lemma, in cyclic]
eltm_morphism [definition, in cyclic]
eltm_id [lemma, in cyclic]
Eltm.aT [variable, in cyclic]
Eltm.dvd_y_x [variable, in cyclic]
Eltm.rT [variable, in cyclic]
Eltm.x [variable, in cyclic]
Eltm.y [variable, in cyclic]
enum [abbreviation, in fintype]
EnumDef [module, in fintype]
enumP [lemma, in fintype]
EnumRank [section, in fintype]
EnumRank.T [variable, in fintype]
EnumSig [module, in fintype]
EnumSocle [constructor, in mxrepresentation]
enumT [lemma, in fintype]
enum_rank_ord [lemma, in fintype]
enum_valK_in [lemma, in fintype]
enum_rank [definition, in fintype]
enum_ordS [lemma, in fintype]
enum_tuple [definition, in tuple]
enum_extremal_groups [definition, in extremal]
enum_valP [lemma, in fintype]
enum_val_bij [lemma, in fintype]
enum_val_ord [lemma, in fintype]
enum_default [lemma, in fintype]
enum_val_nth [lemma, in fintype]
enum_mem [definition, in fintype]
enum_rankK_in [lemma, in fintype]
enum_rank_bij [lemma, in fintype]
enum_uniq [lemma, in fintype]
enum_tupleP [lemma, in tuple]
enum_rankK [lemma, in fintype]
enum_rank_inj [lemma, in fintype]
enum_valK [lemma, in fintype]
enum_rank_in [definition, in fintype]
enum_val_bij_in [lemma, in fintype]
enum_val [definition, in fintype]
enum_val_inj [lemma, in fintype]
enum_rank_subproof [lemma, in fintype]
enum0 [lemma, in fintype]
enum1 [lemma, in fintype]
enveloping_algebra_mx [definition, in mxrepresentation]
envelop_mx_ring [lemma, in mxrepresentation]
envelop_mxP [lemma, in mxrepresentation]
envelop_mxM [lemma, in mxrepresentation]
envelop_mx1 [lemma, in mxrepresentation]
envelop_mx_id [lemma, in mxrepresentation]
EqAllPairs [section, in seq]
EqAllPairs.f [variable, in seq]
EqAllPairs.R [variable, in seq]
EqAllPairs.S [variable, in seq]
EqAllPairs.T [variable, in seq]
eqbE [lemma, in eqtype]
eqbP [lemma, in eqtype]
eqb_id [lemma, in eqtype]
EqConnect [section, in fingraph]
EqConnect.T [variable, in fingraph]
eqE [lemma, in eqtype]
eqEcard [lemma, in finset]
eqEproper [lemma, in finset]
eqEsubset [lemma, in finset]
eqfun [definition, in ssrfun]
EqFun [section, in eqtype]
EqFun.aT [variable, in eqtype]
EqFun.Endo [section, in eqtype]
EqFun.Endo.f [variable, in eqtype]
EqFun.Endo.T [variable, in eqtype]
EqFun.Exo [section, in eqtype]
EqFun.Exo.aT [variable, in eqtype]
EqFun.Exo.D [variable, in eqtype]
EqFun.Exo.f [variable, in eqtype]
EqFun.Exo.g [variable, in eqtype]
EqFun.Exo.rT [variable, in eqtype]
EqFun.f [variable, in eqtype]
EqFun.h [variable, in eqtype]
EqFun.k [variable, in eqtype]
EqFun.rT1 [variable, in eqtype]
EqFun.rT2 [variable, in eqtype]
eqg_mx_abs_irr [lemma, in mxrepresentation]
eqg_repr_proof [lemma, in mxrepresentation]
eqg_mx_faithful [lemma, in mxrepresentation]
eqg_mx_irr [lemma, in mxrepresentation]
eqg_repr [definition, in mxrepresentation]
EqImage [section, in fintype]
EqImage.T [variable, in fintype]
EqImage.T' [variable, in fintype]
EqIso [section, in quotient]
EqIso.eqGH [variable, in quotient]
EqIso.G [variable, in quotient]
EqIso.gT [variable, in quotient]
EqIso.H [variable, in quotient]
EqMap [section, in seq]
EqMap.f [variable, in seq]
EqMap.Hf [variable, in seq]
EqMap.n0 [variable, in seq]
EqMap.T1 [variable, in seq]
EqMap.T2 [variable, in seq]
EqMap.x1 [variable, in seq]
EqMap.x2 [variable, in seq]
EqMask [section, in seq]
EqMask.n0 [variable, in seq]
EqMask.T [variable, in seq]
eqmx [definition, in mxalgebra]
eqmxMfree [lemma, in mxalgebra]
eqmxMfull [lemma, in mxalgebra]
eqmxMr [lemma, in mxalgebra]
eqmxP [lemma, in mxalgebra]
eqmx_semisimple [lemma, in mxrepresentation]
eqmx_module [lemma, in mxrepresentation]
eqmx_trans [lemma, in mxalgebra]
eqmx_cast [lemma, in mxalgebra]
eqmx_rstab [lemma, in mxrepresentation]
eqmx_sum_nop [definition, in mxalgebra]
eqmx_rstabs [lemma, in mxrepresentation]
eqmx_scale [lemma, in mxalgebra]
eqmx_iso [lemma, in mxrepresentation]
eqmx_rank [lemma, in mxalgebra]
eqmx_eq0 [lemma, in mxalgebra]
eqmx_opp [lemma, in mxalgebra]
eqmx_sums [lemma, in mxalgebra]
eqmx_conform [lemma, in mxalgebra]
eqmx_refl [lemma, in mxalgebra]
eqmx_sym [lemma, in mxalgebra]
eqmx0 [lemma, in mxalgebra]
eqmx0P [lemma, in mxalgebra]
eqn [definition, in ssrnat]
eqnE [lemma, in ssrnat]
eqnP [lemma, in ssrnat]
eqn_mul2r [lemma, in ssrnat]
eqn_pmul2l [lemma, in ssrnat]
eqn_pmul2r [lemma, in ssrnat]
eqn_exp2r [lemma, in ssrnat]
eqn_mul2l [lemma, in ssrnat]
eqn_leq [lemma, in ssrnat]
eqn_mul [lemma, in div]
eqn_exp2l [lemma, in ssrnat]
eqn_addl [lemma, in ssrnat]
eqn_mod_dvd [lemma, in div]
eqn_mul1 [lemma, in ssrnat]
eqn_minl [lemma, in ssrnat]
eqn_dvd [lemma, in div]
eqn_minr [lemma, in ssrnat]
eqn_maxl [lemma, in ssrnat]
eqn_addr [lemma, in ssrnat]
eqn_sqr [lemma, in ssrnat]
eqn_maxr [lemma, in ssrnat]
eqn_div [lemma, in div]
eqn0Ngt [lemma, in ssrnat]
eqn0_xor_gt0 [inductive, in ssrnat]
eqP [lemma, in eqtype]
eqp [definition, in poly]
EqPath [section, in path]
EqPath.e [variable, in path]
EqPath.n0 [variable, in path]
EqPath.T [variable, in path]
EqPath.x0_cycle [variable, in path]
EqPcore [section, in pgroup]
EqPcore.gT [variable, in pgroup]
EqPmap [section, in seq]
EqPmapSub [section, in seq]
EqPmapSub.p [variable, in seq]
EqPmapSub.sT [variable, in seq]
EqPmapSub.T [variable, in seq]
EqPmap.aT [variable, in seq]
EqPmap.f [variable, in seq]
EqPmap.fK [variable, in seq]
EqPmap.g [variable, in seq]
EqPmap.rT [variable, in seq]
eqpP [lemma, in poly]
EqPred [section, in eqtype]
EqPred.b [variable, in eqtype]
EqPred.T [variable, in eqtype]
EqPred.T2 [variable, in eqtype]
EqPred.u [variable, in eqtype]
EqPred.x [variable, in eqtype]
EqPred.y [variable, in eqtype]
EqPred.z [variable, in eqtype]
eqpxx [lemma, in poly]
eqp_map [lemma, in poly]
eqp_sym [lemma, in poly]
eqp_trans [lemma, in poly]
eqp0E [lemma, in poly]
eqrel [definition, in ssrfun]
eqseq [definition, in seq]
EqSeq [section, in seq]
eqseqE [lemma, in seq]
eqseqP [lemma, in seq]
eqseq_rcons [lemma, in seq]
eqseq_cons [lemma, in seq]
eqseq_cat [lemma, in seq]
eqseq_class [definition, in seq]
eqseq_rot [lemma, in seq]
EqSeq.Filters [section, in seq]
EqSeq.Filters.a [variable, in seq]
EqSeq.n0 [variable, in seq]
EqSeq.T [variable, in seq]
EqSeq.x0 [variable, in seq]
eqSS [lemma, in ssrnat]
eqsVneq [lemma, in finset]
EqTheory [section, in finfun]
EqTheory.aT [variable, in finfun]
EqTheory.Partial [section, in finfun]
EqTheory.Partial.d [variable, in finfun]
EqTheory.Partial.y0 [variable, in finfun]
EqTheory.rT [variable, in finfun]
EqTrajectory [section, in path]
EqTrajectory.f [variable, in path]
EqTrajectory.T [variable, in path]
EqTuple [section, in tuple]
EqTuple.n [variable, in tuple]
EqTuple.T [variable, in tuple]
eqtype [library]
EqTypePred [module, in eqtype]
EqTypePredSig [module, in eqtype]
EqTypePredSig.sort [axiom, in eqtype]
Equality [module, in eqtype]
Equality.axiom [definition, in eqtype]
Equality.class [definition, in eqtype]
Equality.ClassDef [section, in eqtype]
Equality.ClassDef.cT [variable, in eqtype]
Equality.ClassDef.T [variable, in eqtype]
Equality.class_of [abbreviation, in eqtype]
Equality.clone [definition, in eqtype]
Equality.Exports.EqMixin [abbreviation, in eqtype]
Equality.Exports.eqType [abbreviation, in eqtype]
Equality.Exports.EqType [abbreviation, in eqtype]
Equality.Mixin [constructor, in eqtype]
Equality.mixin_of [record, in eqtype]
Equality.op [projection, in eqtype]
Equality.pack [definition, in eqtype]
Equality.Pack [constructor, in eqtype]
Equality.sort [projection, in eqtype]
Equality.type [record, in eqtype]
equivmx [definition, in mxalgebra]
equivmx_spec [definition, in mxalgebra]
equivPif [lemma, in ssrbool]
equivPifn [lemma, in ssrbool]
eqVneq [lemma, in eqtype]
eqVproper [lemma, in finset]
eqxx [abbreviation, in eqtype]
eq_proper [lemma, in fintype]
eq_homgr [lemma, in morphism]
eq_from_nth [lemma, in seq]
eq_Mod8_D8 [lemma, in extremal]
eq_card1 [lemma, in fintype]
eq_mkseq [lemma, in seq]
eq_partn [lemma, in prime]
eq_sorted [lemma, in path]
eq_primes [lemma, in prime]
eq_rank_unitmx [lemma, in mxalgebra]
eq_can [lemma, in ssrfun]
eq_subxx [lemma, in fintype]
eq_preimset [lemma, in finset]
eq_imset [lemma, in finset]
eq_pHall [lemma, in pgroup]
eq_finv [lemma, in fingraph]
eq_subset_r [lemma, in fintype]
eq_in_pHall [lemma, in pgroup]
eq_pnat [lemma, in prime]
eq_disjoint [lemma, in fintype]
eq_fpath [lemma, in fingraph]
eq_prim_root_expr [lemma, in poly]
eq_iteri [lemma, in ssrnat]
eq_big_idx_seq [lemma, in bigop]
eq_pred1 [lemma, in fingraph]
eq_filter [lemma, in seq]
eq_has [lemma, in seq]
eq_row_sub [lemma, in mxalgebra]
eq_from_tnth [lemma, in tuple]
eq_p'Hall [lemma, in pgroup]
eq_refl [lemma, in eqtype]
eq_froot [lemma, in fingraph]
eq_bigmax [lemma, in bigop]
eq_tag [lemma, in eqtype]
eq_mulgV1 [lemma, in fingroup]
eq_in_filter [lemma, in seq]
eq_bigl [lemma, in bigop]
eq_pmap [lemma, in seq]
eq_has_r [lemma, in seq]
eq_bigmax_cond [lemma, in bigop]
eq_Aut [lemma, in automorphism]
eq_roots [lemma, in fingraph]
eq_homgl [lemma, in morphism]
eq_p'core [lemma, in pgroup]
eq_pcore [lemma, in pgroup]
eq_big_perm [lemma, in bigop]
eq_big [lemma, in bigop]
eq_op [definition, in eqtype]
eq_bij [lemma, in ssrfun]
eq_count [lemma, in seq]
eq_constt [lemma, in pgroup]
eq_invg_mul [lemma, in fingroup]
eq_card_trans [lemma, in fintype]
eq_Hall_pcore [lemma, in pgroup]
eq_bigr [lemma, in bigop]
eq_choose [lemma, in choice]
eq_limg_ker0 [lemma, in vector]
eq_comparable [definition, in eqtype]
eq_in_morphim [lemma, in morphism]
eq_negn [lemma, in prime]
eq_axiomK [lemma, in eqtype]
eq_ex_minn [lemma, in ssrnat]
eq_row_mx [lemma, in matrix]
eq_mulVg1 [lemma, in fingroup]
eq_pick [lemma, in fintype]
eq_genmx [lemma, in mxalgebra]
eq_piP [lemma, in prime]
eq_big_op_seq [lemma, in bigop]
eq_in_partn [lemma, in prime]
eq_iter [lemma, in ssrnat]
eq_root [lemma, in fingraph]
eq_invF [lemma, in fintype]
eq_card_prod [lemma, in fintype]
eq_in_imset2 [lemma, in finset]
eq_in_pnat [lemma, in prime]
eq_enum [lemma, in fintype]
eq_ex_maxn [lemma, in ssrnat]
eq_irrelevance [lemma, in eqtype]
eq_pcycle_mem [lemma, in perm]
eq_codom [lemma, in fintype]
eq_invg_sym [lemma, in fingroup]
eq_invg1 [lemma, in fingroup]
eq_sym [lemma, in eqtype]
eq_fconnect [lemma, in fingraph]
eq_cardT [lemma, in fintype]
eq_connect0 [lemma, in fingraph]
eq_xchoose [lemma, in choice]
eq_binP [lemma, in ssrnat]
eq_block_mx [lemma, in matrix]
eq_all [lemma, in seq]
eq_rowg [lemma, in mxabelem]
eq_froots [lemma, in fingraph]
eq_big_idx [lemma, in bigop]
eq_connect [lemma, in fingraph]
eq_leq [lemma, in ssrnat]
eq_subset [lemma, in fintype]
eq_in_imset [lemma, in finset]
eq_forallb [lemma, in fintype]
eq_path [lemma, in path]
eq_iterop [lemma, in ssrnat]
eq_disjoint0 [lemma, in fintype]
eq_sorted_irr [lemma, in path]
eq_disjoint1 [lemma, in fintype]
eq_image [lemma, in fintype]
eq_proper_r [lemma, in fintype]
eq_subG_cyclic [lemma, in cyclic]
eq_in_pcore [lemma, in pgroup]
eq_inj [lemma, in ssrfun]
eq_n_comp_r [lemma, in fingraph]
eq_col_mx [lemma, in matrix]
eq_expg_mod_order [lemma, in cyclic]
eq_morphim [lemma, in morphism]
eq_fcard [lemma, in fingraph]
eq_card [lemma, in fintype]
eq_homGrp [lemma, in presentation]
eq_card0 [lemma, in fintype]
eq_find [lemma, in seq]
eq_existsb [lemma, in fintype]
eq_disjoint_r [lemma, in fintype]
eq_comp [lemma, in ssrfun]
eq_mem [definition, in ssrbool]
eq_abelian_type_isog [lemma, in abelian]
eq_p_elt [lemma, in pgroup]
eq_big_op [lemma, in bigop]
eq_cpairZ [lemma, in center]
eq_p'group [lemma, in pgroup]
eq_all_r [lemma, in seq]
eq_row_base [lemma, in mxalgebra]
eq_in_map [lemma, in seq]
eq_lapp [lemma, in vector]
eq_map [lemma, in seq]
eq_Tagged [lemma, in eqtype]
eq_pgroup [lemma, in pgroup]
eq_n_comp [lemma, in fingraph]
eq_card_sub [lemma, in fintype]
Eq0NotPos [constructor, in ssrnat]
erefl [definition, in ssrfun]
ErV [abbreviation, in mxabelem]
esym [definition, in ssrfun]
esymK [lemma, in ssrfun]
etrans [definition, in ssrfun]
etrans_id [lemma, in ssrfun]
euclid [lemma, in prime]
euclid_exp [lemma, in prime]
euclid1 [lemma, in prime]
Euler [lemma, in cyclic]
eval [abbreviation, in mxrepresentation]
EvalPolynomial [section, in poly]
EvalPolynomial.n [variable, in poly]
EvalPolynomial.prim_z [variable, in poly]
EvalPolynomial.R [variable, in poly]
EvalPolynomial.z [variable, in poly]
eval_mxmodule [lemma, in mxrepresentation]
even_prime [lemma, in prime]
evf [definition, in vector]
evfK [lemma, in vector]
ev_of_tupleK [lemma, in vector]
ev_ax [abbreviation, in eqtype]
ev_of_tuple [definition, in vector]
ev2l [definition, in vector]
exchange_big_dep_nat [lemma, in bigop]
exchange_big_nat [lemma, in bigop]
exchange_big_dep [lemma, in bigop]
exchange_big [lemma, in bigop]
exFP [definition, in fintype]
existsP [lemma, in fintype]
exists_inP [lemma, in fintype]
exists_comps [lemma, in jordanholder]
exists_acomps [lemma, in jordanholder]
ExMaxn [section, in ssrnat]
ExMaxnSpec [constructor, in ssrnat]
ExMaxn.exP [variable, in ssrnat]
ExMaxn.m [variable, in ssrnat]
ExMaxn.P [variable, in ssrnat]
ExMaxn.ubP [variable, in ssrnat]
ExMinn [section, in ssrnat]
ExMinnSpec [constructor, in ssrnat]
ExMinn.exP [variable, in ssrnat]
ExMinn.P [variable, in ssrnat]
expand_cofactor [lemma, in matrix]
expand_det_col [lemma, in matrix]
expand_det_row [lemma, in matrix]
expgn [definition, in fingroup]
expgnC [lemma, in fingroup]
expgnE [lemma, in fingroup]
expgnK [lemma, in cyclic]
expgn_zneg [lemma, in cyclic]
expgn_inv [definition, in cyclic]
expgn_add [lemma, in fingroup]
expgn_mul [lemma, in fingroup]
expgn_rec [definition, in fingroup]
expgn_znat [lemma, in cyclic]
expgS [lemma, in fingroup]
expgSr [lemma, in fingroup]
expg_mod [lemma, in fingroup]
expg_mod_order [lemma, in fingroup]
expg_order [lemma, in fingroup]
expg_exponent [lemma, in abelian]
expg0 [lemma, in fingroup]
expg1 [lemma, in fingroup]
expIn [lemma, in ssrnat]
expMgn [lemma, in fingroup]
expMg_Rmul [lemma, in commutator]
expn [definition, in ssrnat]
expnE [lemma, in ssrnat]
expnI [lemma, in ssrnat]
expnS [lemma, in ssrnat]
expnSr [lemma, in ssrnat]
expn_eq0 [lemma, in ssrnat]
expn_mulr [lemma, in ssrnat]
expn_add [lemma, in ssrnat]
expn_sub [lemma, in div]
expn_gt0 [lemma, in ssrnat]
expn_addl [definition, in binomial]
expn_rec [definition, in ssrnat]
expn_sum [lemma, in bigop]
expn_mull [lemma, in ssrnat]
expn0 [lemma, in ssrnat]
expn1 [lemma, in ssrnat]
exponent [definition, in abelian]
ExponentAbelem [section, in abelian]
ExponentAbelem.gT [variable, in abelian]
exponentJ [lemma, in abelian]
exponentP [lemma, in abelian]
ExponentPextraspecialTheory [section, in extraspecial]
ExponentPextraspecialTheory.p [variable, in extraspecial]
ExponentPextraspecialTheory.p_pr [variable, in extraspecial]
exponentS [lemma, in abelian]
exponent_morphim [lemma, in abelian]
exponent_dvdn [lemma, in abelian]
exponent_witness [lemma, in abelian]
exponent_special [lemma, in maximal]
exponent_pX1p2 [lemma, in extraspecial]
exponent_pX1p2n [lemma, in extraspecial]
exponent_injm [lemma, in abelian]
exponent_quotient [lemma, in abelian]
exponent_cyclic [lemma, in abelian]
exponent_cycle [lemma, in abelian]
exponent_Hall [lemma, in abelian]
exponent_Ohm1_class2 [lemma, in maximal]
exponent_2extraspecial [lemma, in maximal]
exponent_isog [lemma, in abelian]
exponent_gt0 [lemma, in abelian]
exponent1 [lemma, in abelian]
exponent2_abelem [lemma, in abelian]
Exports [module, in ssralg]
Exports [module, in choice]
Exports [module, in ssralg]
Exports [module, in ssralg]
Exports [module, in ssralg]
Exports [module, in ssralg]
Exports [module, in finalg]
Exports [module, in ssralg]
Exports [module, in ssralg]
Exports [module, in fingroup]
Exports [module, in ssralg]
Exports [module, in ssralg]
Exports [module, in ssralg]
Exports [module, in ssralg]
Exports [module, in finalg]
Exports [module, in fintype]
Exports [module, in ssralg]
Exports [module, in ssralg]
Exports [module, in bigop]
Exports [module, in ssralg]
Exports [module, in finalg]
Exports [module, in finalg]
Exports [module, in eqtype]
Exports [module, in ssralg]
Exports [module, in finalg]
Exports [module, in choice]
Exports [module, in vector]
Exports [module, in finalg]
Exports [module, in ssralg]
Exports [module, in ssralg]
Exports [module, in finalg]
Exports [module, in finalg]
Exports [module, in finalg]
Exports [module, in finalg]
Exports [module, in ssralg]
Exports [module, in gfunctor]
Exports [module, in finalg]
Exports [module, in finalg]
ExpVector [section, in vector]
expVector [definition, in vector]
ExpVector.K [variable, in vector]
ExpVector.V [variable, in vector]
expVgn [lemma, in fingroup]
exp0n [lemma, in ssrnat]
exp1gn [lemma, in fingroup]
exp1n [lemma, in ssrnat]
ExtCprod [section, in center]
ExtCprod.gTH [variable, in center]
ExtCprod.gTK [variable, in center]
ExtCprod.H [variable, in center]
ExtCprod.K [variable, in center]
extend_cyclic_Mho [lemma, in abelian]
extend_group_splitting_field [lemma, in mxrepresentation]
extend_number [definition, in ssrnat]
ExtensionalEquality [section, in ssrfun]
ExtensionalEquality.A [variable, in ssrfun]
ExtensionalEquality.B [variable, in ssrfun]
ExtensionalEquality.C [variable, in ssrfun]
Extensionality [section, in bigop]
Extensionality.idx [variable, in bigop]
Extensionality.op [variable, in bigop]
Extensionality.R [variable, in bigop]
Extensionality.SeqExtension [section, in bigop]
Extensionality.SeqExtension.I [variable, in bigop]
ExternalAction [section, in hall]
ExternalAction.A [variable, in hall]
ExternalAction.aT [variable, in hall]
ExternalAction.FullExtension [section, in hall]
ExternalAction.FullExtension.coGA [variable, in hall]
ExternalAction.FullExtension.solG [variable, in hall]
ExternalAction.G [variable, in hall]
ExternalAction.gT [variable, in hall]
ExternalAction.pi [variable, in hall]
ExternalAction.to [variable, in hall]
ExternalDirProd [section, in gproduct]
ExternalDirProd.gT1 [variable, in gproduct]
ExternalDirProd.gT2 [variable, in gproduct]
ExternalSDirProd [section, in gproduct]
ExternalSDirProd.A [variable, in gproduct]
ExternalSDirProd.aT [variable, in gproduct]
ExternalSDirProd.D [variable, in gproduct]
ExternalSDirProd.G [variable, in gproduct]
ExternalSDirProd.R [variable, in gproduct]
ExternalSDirProd.rT [variable, in gproduct]
ExternalSDirProd.sAD [variable, in gproduct]
ExternalSDirProd.sGR [variable, in gproduct]
ExternalSDirProd.to [variable, in gproduct]
external_action_im_coprime [lemma, in hall]
extgK [abbreviation, in extremal]
extprod_baseFinGroupType [definition, in gproduct]
extprod_mul1g [lemma, in gproduct]
extprod_mulgA [lemma, in gproduct]
extprod_groupMixin [definition, in gproduct]
extprod_invg [definition, in gproduct]
extprod_mulVg [lemma, in gproduct]
extprod_mulg [definition, in gproduct]
Extraspecial [section, in mxabelem]
Extraspecial [section, in maximal]
extraspecial [definition, in maximal]
extraspecial [library]
extraspecial_nonabelian [lemma, in maximal]
extraspecial_prime [lemma, in maximal]
extraspecial_repr_structure [lemma, in mxabelem]
extraspecial_structure [lemma, in maximal]
Extraspecial.Basic [section, in maximal]
Extraspecial.Basic.esS [variable, in maximal]
Extraspecial.Basic.pS [variable, in maximal]
Extraspecial.Basic.S [variable, in maximal]
Extraspecial.esS [variable, in mxabelem]
Extraspecial.ExtraspecialFormspace [section, in maximal]
Extraspecial.ExtraspecialFormspace.esG [variable, in maximal]
Extraspecial.ExtraspecialFormspace.G [variable, in maximal]
Extraspecial.ExtraspecialFormspace.pG [variable, in maximal]
Extraspecial.F [variable, in mxabelem]
Extraspecial.ffulU [variable, in mxabelem]
Extraspecial.F'S [variable, in mxabelem]
Extraspecial.gT [variable, in maximal]
Extraspecial.gT [variable, in mxabelem]
Extraspecial.m [variable, in mxabelem]
Extraspecial.n [variable, in mxabelem]
Extraspecial.oSpn [variable, in mxabelem]
Extraspecial.p [variable, in maximal]
Extraspecial.p [variable, in mxabelem]
Extraspecial.pS [variable, in mxabelem]
Extraspecial.rS [variable, in mxabelem]
Extraspecial.rT [variable, in maximal]
Extraspecial.S [variable, in mxabelem]
Extraspecial.simU [variable, in mxabelem]
Extraspecial.splitF [variable, in mxabelem]
Extraspecial.StructureCorollaries [section, in maximal]
Extraspecial.StructureCorollaries.esS [variable, in maximal]
Extraspecial.StructureCorollaries.pS [variable, in maximal]
Extraspecial.StructureCorollaries.S [variable, in maximal]
Extraspecial.U [variable, in mxabelem]
Extrema [section, in fintype]
Extremal [module, in extremal]
extremal [library]
ExtremalTheory [section, in extremal]
ExtremalTheory.DihedralGroup [section, in extremal]
ExtremalTheory.DihedralGroup.Dihedral_extension.even_p [variable, in extremal]
ExtremalTheory.DihedralGroup.Dihedral_extension.p_gt1 [variable, in extremal]
ExtremalTheory.DihedralGroup.Dihedral_extension.p [variable, in extremal]
ExtremalTheory.DihedralGroup.Dihedral_extension [section, in extremal]
ExtremalTheory.DihedralGroup.q [variable, in extremal]
ExtremalTheory.DihedralGroup.q_gt1 [variable, in extremal]
ExtremalTheory.ExtremalClass [section, in extremal]
ExtremalTheory.ExtremalClass.G [variable, in extremal]
ExtremalTheory.ExtremalClass.gT [variable, in extremal]
ExtremalTheory.ExtremalStructure [section, in extremal]
ExtremalTheory.ExtremalStructure.G [variable, in extremal]
ExtremalTheory.ExtremalStructure.gT [variable, in extremal]
ExtremalTheory.ExtremalStructure.n [variable, in extremal]
ExtremalTheory.ExtremalStructure.x [variable, in extremal]
ExtremalTheory.ExtremalStructure.y [variable, in extremal]
ExtremalTheory.ModularGroup [section, in extremal]
ExtremalTheory.ModularGroup.n [variable, in extremal]
ExtremalTheory.ModularGroup.n_gt2 [variable, in extremal]
ExtremalTheory.ModularGroup.p [variable, in extremal]
ExtremalTheory.ModularGroup.p_pr [variable, in extremal]
ExtremalTheory.Quaternion [section, in extremal]
ExtremalTheory.Quaternion.n [variable, in extremal]
ExtremalTheory.Quaternion.n_gt2 [variable, in extremal]
extremal_group_type [inductive, in extremal]
extremal_group_eqMixin [definition, in extremal]
extremal_group_countMixin [definition, in extremal]
extremal_generators_facts [lemma, in extremal]
extremal_group_finMixin [definition, in extremal]
extremal_class [definition, in extremal]
extremal_group_finType [definition, in extremal]
extremal_group_countType [definition, in extremal]
extremal_group_choiceType [definition, in extremal]
extremal_group_eqType [definition, in extremal]
extremal_group_choiceMixin [definition, in extremal]
extremal_generators [definition, in extremal]
Extremal.a [definition, in extremal]
Extremal.act_dom [lemma, in extremal]
Extremal.act_morphism [definition, in extremal]
Extremal.aut_dvdn [lemma, in extremal]
Extremal.aut_of [definition, in extremal]
Extremal.B [abbreviation, in extremal]
Extremal.b [definition, in extremal]
Extremal.base_act [definition, in extremal]
Extremal.card [lemma, in extremal]
Extremal.Construction [section, in extremal]
Extremal.Construction.e [variable, in extremal]
Extremal.Construction.p [variable, in extremal]
Extremal.Construction.p_gt1 [variable, in extremal]
Extremal.Construction.q [variable, in extremal]
Extremal.Construction.q_gt1 [variable, in extremal]
Extremal.gact [definition, in extremal]
Extremal.Grp [lemma, in extremal]
Extremal.gtype [definition, in extremal]
extremal2 [definition, in extremal]
extremal2_structure [lemma, in extremal]
Extrema.F [variable, in fintype]
Extrema.I [variable, in fintype]
Extrema.i0 [variable, in fintype]
Extrema.P [variable, in fintype]
Extrema.Pi0 [variable, in fintype]
ExtremumSpec [constructor, in fintype]
extremum_spec [inductive, in fintype]
ExtSdprodm [section, in gproduct]
ExtSdprodm.actf [variable, in gproduct]
ExtSdprodm.aT [variable, in gproduct]
ExtSdprodm.fH [variable, in gproduct]
ExtSdprodm.fK [variable, in gproduct]
ExtSdprodm.gT [variable, in gproduct]
ExtSdprodm.H [variable, in gproduct]
ExtSdprodm.K [variable, in gproduct]
ExtSdprodm.rT [variable, in gproduct]
ExtSdprodm.to [variable, in gproduct]
ext_coprime_Hall_subset [lemma, in hall]
ext_coprime_Hall_trans [lemma, in hall]
ext_coprime_Hall_exists [lemma, in hall]
ext_coprime_quotient_cent [lemma, in hall]
ext_norm_conj_cent [lemma, in hall]
ex_maxnormal_ntrivg [lemma, in gseries]
ex_maxn_spec [inductive, in ssrnat]
ex_maxnP [lemma, in ssrnat]
ex_minset [lemma, in finset]
ex_maxgroup [lemma, in fingroup]
ex_minn_spec [inductive, in ssrnat]
ex_minnP [lemma, in ssrnat]
ex_mingroup [lemma, in fingroup]
ex_minn [definition, in ssrnat]
ex_maxset [lemma, in finset]
ex_maxn [definition, in ssrnat]
ex_maxn_subproof [lemma, in ssrnat]
E_ [abbreviation, in mxrepresentation]
E_G [abbreviation, in mxrepresentation]
E_G [abbreviation, in mxrepresentation]
E_G [abbreviation, in mxrepresentation]
e_ [abbreviation, in mxrepresentation]
e0 [abbreviation, in mxrepresentation]



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 (14626 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 (165 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 (112 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 (7292 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 (761 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 (250 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 (390 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 (84 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 (3144 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 (126 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 (28 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 (2221 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 (53 entries)