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)

I

id [abbreviation, in ssrfun]
idempotent [definition, in ssrfun]
IdentityMorphism [section, in morphism]
IdentityMorphism.gT [variable, in morphism]
idfun [definition, in ssrfun]
idGfun [definition, in gfunctor]
idGfun_cont [lemma, in gfunctor]
idGfun_monotonic [lemma, in gfunctor]
idGfun_closed [lemma, in gfunctor]
idm [definition, in morphism]
idmxE [lemma, in matrix]
idm_morphism [definition, in morphism]
idm_morphM [lemma, in morphism]
idP [lemma, in ssrbool]
idPn [lemma, in ssrbool]
ifactm [definition, in morphism]
ifactmE [lemma, in morphism]
ifE [lemma, in ssrbool]
iffLR [lemma, in ssreflect]
iffLRn [lemma, in ssreflect]
iffP [lemma, in ssrbool]
iffRL [lemma, in ssreflect]
iffRLn [lemma, in ssreflect]
ifnE [lemma, in ssrnat]
ifnz [definition, in prime]
ifnzP [lemma, in prime]
IfnzPos [constructor, in prime]
IfnzZero [constructor, in prime]
ifnz_spec [inductive, in prime]
ifn_expr [definition, in ssrnat]
ifP [lemma, in ssrbool]
ifPn [lemma, in ssrbool]
IfSpecFalse [constructor, in ssrbool]
IfSpecTrue [constructor, in ssrbool]
if_arg [lemma, in ssrbool]
if_expr [definition, in ssrbool]
if_same [lemma, in ssrbool]
if_spec [inductive, in ssrbool]
if_neg [lemma, in ssrbool]
iG [abbreviation, in mxrepresentation]
iinv [definition, in fintype]
iinv_proof [lemma, in fintype]
iinv_f [lemma, in fintype]
Image [section, in fintype]
image [definition, in fintype]
imageP [lemma, in fintype]
image_pred0 [lemma, in fintype]
image_injP [lemma, in fintype]
image_f [lemma, in fintype]
image_iinv [lemma, in fintype]
image_pre [lemma, in fintype]
image_codom [lemma, in fintype]
Image.Def [section, in fintype]
Image.Def.A [variable, in fintype]
Image.Def.injf [variable, in fintype]
Image.f [variable, in fintype]
Image.T [variable, in fintype]
Image.T' [variable, in fintype]
imHg_eq [abbreviation, in finmodule]
implybb [lemma, in ssrbool]
implybE [lemma, in ssrbool]
implybF [lemma, in ssrbool]
implybN [lemma, in ssrbool]
implybNN [lemma, in ssrbool]
implybT [lemma, in ssrbool]
implyb_idr [lemma, in ssrbool]
implyb_idl [lemma, in ssrbool]
implyb_id2l [lemma, in ssrbool]
implyFb [lemma, in ssrbool]
implyNb [lemma, in ssrbool]
implyP [lemma, in ssrbool]
implyTb [lemma, in ssrbool]
imprimitivity_system [definition, in primitive_action]
Imset [module, in finset]
imset [abbreviation, in finset]
ImsetCurry [section, in finset]
ImsetCurry.aT1 [variable, in finset]
ImsetCurry.aT2 [variable, in finset]
ImsetCurry.Curry [section, in finset]
ImsetCurry.Curry.A1 [variable, in finset]
ImsetCurry.Curry.A2 [variable, in finset]
ImsetCurry.Curry.D1 [variable, in finset]
ImsetCurry.Curry.D2 [variable, in finset]
ImsetCurry.f [variable, in finset]
ImsetCurry.rT [variable, in finset]
imsetI [lemma, in finset]
imsetP [lemma, in finset]
imsetS [lemma, in finset]
ImsetSig [module, in finset]
ImsetSig.imset [axiom, in finset]
ImsetSig.imsetE [axiom, in finset]
ImsetSig.imset2 [axiom, in finset]
ImsetSig.imset2E [axiom, in finset]
imsetU [lemma, in finset]
imsetU1 [lemma, in finset]
imset_injP [lemma, in finset]
imset_unlock [definition, in finset]
imset_card [lemma, in finset]
imset_mulgm [lemma, in gproduct]
imset_set1 [lemma, in finset]
imset_autE [lemma, in automorphism]
imset_coset [lemma, in quotient]
imset_comp [lemma, in finset]
imset_def [abbreviation, in finset]
imset_proper [lemma, in finset]
Imset.imset [definition, in finset]
Imset.imsetE [lemma, in finset]
Imset.imset2 [definition, in finset]
Imset.imset2E [lemma, in finset]
imset0 [lemma, in finset]
imset2 [abbreviation, in finset]
imset2P [lemma, in finset]
imset2S [lemma, in finset]
imset2Sl [lemma, in finset]
Imset2spec [constructor, in finset]
imset2Sr [lemma, in finset]
imset2Ul [lemma, in finset]
imset2Ur [lemma, in finset]
imset2_set1r [lemma, in finset]
imset2_unlock [definition, in finset]
imset2_set1l [lemma, in finset]
imset2_spec [inductive, in finset]
imset2_pair [lemma, in finset]
imset2_def [abbreviation, in finset]
im_conjgm_norm [lemma, in automorphism]
im_cyclem [lemma, in cyclic]
im_restr_perm [lemma, in action]
im_xcprodml [lemma, in center]
im_qisom [lemma, in quotient]
im_sdpair_norm [lemma, in gproduct]
im_sdpair_TI [lemma, in gproduct]
im_actperm_Aut [lemma, in action]
im_cpair [lemma, in center]
im_xcprodm [lemma, in center]
im_cpair_cent [lemma, in center]
im_rcosets_pcycle_transversal [lemma, in finmodule]
im_abelem_rV [lemma, in mxabelem]
im_subg [lemma, in morphism]
im_Aut_isom [lemma, in automorphism]
im_rVabelem [lemma, in mxabelem]
im_coset [lemma, in quotient]
im_sdpair [lemma, in gproduct]
im_cprodm [lemma, in gproduct]
im_permV [lemma, in perm]
im_sdprodm [lemma, in gproduct]
im_invm [lemma, in morphism]
im_eltm [lemma, in cyclic]
im_ifactm [lemma, in morphism]
im_xcprodmr [lemma, in center]
im_dprodm [lemma, in gproduct]
im_Zpm [lemma, in cyclic]
im_xsdprodm [lemma, in gproduct]
im_perm_on [lemma, in perm]
im_autm [lemma, in automorphism]
im_cpair_cprod [lemma, in center]
im_restrm [lemma, in morphism]
im_sgval [lemma, in morphism]
im_qisom_proof [lemma, in quotient]
im_actm [lemma, in action]
im_sdprodm2 [lemma, in gproduct]
im_idm [lemma, in morphism]
im_sdprodm1 [lemma, in gproduct]
im_Zp_unitm [lemma, in cyclic]
inA [abbreviation, in hall]
incr_nth [definition, in seq]
index [definition, in seq]
indexg [definition, in fingroup]
indexgg [lemma, in fingroup]
indexgI [lemma, in fingroup]
indexgS [lemma, in fingroup]
indexg_gt1 [lemma, in fingroup]
indexg_eq1 [lemma, in fingroup]
indexg_gt0 [lemma, in fingroup]
indexg1 [lemma, in fingroup]
indexJg [lemma, in fingroup]
indexMg [lemma, in fingroup]
indexSg [lemma, in fingroup]
index_quotient_ker [lemma, in quotient]
index_quotient_eq [lemma, in quotient]
index_injm [lemma, in quotient]
index_cat [lemma, in seq]
index_morphim [lemma, in quotient]
index_extremal_group_type [definition, in extremal]
index_size [lemma, in seq]
index_mem [lemma, in seq]
index_uniq [lemma, in seq]
index_head [lemma, in seq]
index_cent1 [lemma, in action]
index_enum_ord [lemma, in fintype]
index_last [lemma, in seq]
index_cosetpre [lemma, in quotient]
index_morphim_ker [lemma, in quotient]
index_iota [definition, in bigop]
index_enum [definition, in bigop]
index_morphpre [lemma, in quotient]
index_map [lemma, in seq]
index_quotient [lemma, in quotient]
index_maxnormal_sol_prime [lemma, in maximal]
index1g [lemma, in fingroup]
index2_normal [lemma, in fingroup]
inE [definition, in seq]
inE [definition, in finset]
inE [definition, in ssrbool]
inE [definition, in seq]
infH [abbreviation, in action]
inG [abbreviation, in hall]
inH [abbreviation, in action]
injA [definition, in hall]
Injections [section, in ssrfun]
InjectionsTheory [section, in ssrfun]
InjectionsTheory.A [variable, in ssrfun]
InjectionsTheory.B [variable, in ssrfun]
InjectionsTheory.C [variable, in ssrfun]
InjectionsTheory.f [variable, in ssrfun]
InjectionsTheory.g [variable, in ssrfun]
InjectionsTheory.h [variable, in ssrfun]
Injections.aT [variable, in ssrfun]
Injections.f [variable, in ssrfun]
Injections.rT [variable, in ssrfun]
injective [definition, in ssrfun]
Injectiveb [section, in fintype]
injectiveb [definition, in fintype]
Injectiveb.aT [variable, in fintype]
Injectiveb.f [variable, in fintype]
Injectiveb.rT [variable, in fintype]
injectiveP [lemma, in fintype]
injectivePn [lemma, in fintype]
InjEqMixin [definition, in eqtype]
InjFactm [section, in morphism]
InjFactm.aT [variable, in morphism]
InjFactm.D [variable, in morphism]
InjFactm.f [variable, in morphism]
InjFactm.g [variable, in morphism]
InjFactm.G [variable, in morphism]
InjFactm.gT [variable, in morphism]
InjFactm.injf [variable, in morphism]
InjFactm.rT [variable, in morphism]
injF_bij [lemma, in fintype]
injF_codom [lemma, in fintype]
injG [definition, in hall]
injgz [definition, in center]
injH [definition, in center]
injK [definition, in center]
Injm [section, in pgroup]
InjmAbelem [section, in abelian]
InjmAbelem.aT [variable, in abelian]
InjmAbelem.D [variable, in abelian]
InjmAbelem.f [variable, in abelian]
InjmAbelem.G [variable, in abelian]
InjmAbelem.injf [variable, in abelian]
InjmAbelem.rT [variable, in abelian]
InjmAbelem.sGD [variable, in abelian]
InjmAut [section, in automorphism]
InjmAutIn [section, in action]
InjmAutIn.D [variable, in action]
InjmAutIn.f [variable, in action]
InjmAutIn.G [variable, in action]
InjmAutIn.gT [variable, in action]
InjmAutIn.H [variable, in action]
InjmAutIn.injf [variable, in action]
InjmAutIn.rT [variable, in action]
InjmAutIn.sGD [variable, in action]
InjmAutIn.sHG [variable, in action]
InjmAut.D [variable, in automorphism]
InjmAut.f [variable, in automorphism]
InjmAut.G [variable, in automorphism]
InjmAut.gT [variable, in automorphism]
InjmAut.injf [variable, in automorphism]
InjmAut.rT [variable, in automorphism]
InjmAut.sGD [variable, in automorphism]
InjmChar [section, in automorphism]
InjmChar.aT [variable, in automorphism]
InjmChar.D [variable, in automorphism]
InjmChar.f [variable, in automorphism]
InjmChar.injf [variable, in automorphism]
InjmChar.rT [variable, in automorphism]
injmF [lemma, in gfunctor]
injmF_sub [lemma, in gfunctor]
injmI [lemma, in morphism]
injmK [lemma, in morphism]
InjmMax [section, in gseries]
InjmMax.D [variable, in gseries]
InjmMax.f [variable, in gseries]
InjmMax.G [variable, in gseries]
InjmMax.gT [variable, in gseries]
InjmMax.H [variable, in gseries]
InjmMax.injf [variable, in gseries]
InjmMax.K [variable, in gseries]
InjmMax.rT [variable, in gseries]
injmP [lemma, in morphism]
injmSK [lemma, in morphism]
injm_norm [lemma, in morphism]
injm_pElem [lemma, in abelian]
injm_special [lemma, in maximal]
injm_Aut_sub [lemma, in action]
injm_dprodm [lemma, in gproduct]
injm_nElem [lemma, in abelian]
injm_Zpm [lemma, in cyclic]
injm_pcore [lemma, in pgroup]
injm_sdprodm [lemma, in gproduct]
injm_grank [lemma, in abelian]
injm_extraspecial [lemma, in maximal]
injm_cpair1g [lemma, in center]
injm_subcent [lemma, in morphism]
injm_xcprodm [lemma, in center]
injm_comp [lemma, in morphism]
injm_pHall [lemma, in pgroup]
injm_abelian [lemma, in morphism]
injm_cpairg1 [lemma, in center]
injm_subnorm [lemma, in morphism]
injm_faithful [lemma, in action]
injm_conj [lemma, in automorphism]
injm_cent1 [lemma, in morphism]
injm_cprodm [lemma, in gproduct]
injm_pairg1 [lemma, in gproduct]
injm_cyclem [lemma, in cyclic]
injm_xsdprodm [lemma, in gproduct]
injm_pprodm [lemma, in gproduct]
injm_sgval [lemma, in morphism]
injm_maximal_eq [lemma, in gseries]
injm_pseries [lemma, in pgroup]
injm_dprod [lemma, in gproduct]
injm_eltm [lemma, in cyclic]
injm_generator [lemma, in cyclic]
injm_rank [lemma, in abelian]
injm_Ldiv [lemma, in abelian]
injm_invm [lemma, in morphism]
injm_pelt [lemma, in pgroup]
injm_Aut_isom [lemma, in automorphism]
injm_pmaxElem [lemma, in abelian]
injm_pgroup [lemma, in pgroup]
injm_subg [lemma, in morphism]
injm_factm [lemma, in morphism]
injm_abelem [lemma, in abelian]
injm_Aut_full [lemma, in action]
injm_sdprod [lemma, in gproduct]
injm_subcent1 [lemma, in morphism]
injm_factmP [lemma, in morphism]
injm_ifactm [lemma, in morphism]
injm_cyclic [lemma, in cyclic]
injm_Ohm [lemma, in abelian]
injm_cent [lemma, in morphism]
injm_qisom [lemma, in quotient]
injm_pnElem [lemma, in abelian]
injm_actm [lemma, in action]
injm_restrm [lemma, in morphism]
injm_p_rank [lemma, in abelian]
injm_autm [lemma, in automorphism]
injm_pair1g [lemma, in gproduct]
injm_nil [lemma, in nilpotent]
injm_Aut [lemma, in automorphism]
injm_Zp_unitm [lemma, in cyclic]
injm_sdpair2 [lemma, in gproduct]
injm_maximal [lemma, in gseries]
injm_ucn [lemma, in nilpotent]
injm_sol [lemma, in nilpotent]
injm_idm [lemma, in morphism]
injm_Phi [lemma, in maximal]
injm_proper [lemma, in morphism]
injm_Fitting [lemma, in maximal]
injm_morphim_inj [lemma, in morphism]
injm_char [lemma, in automorphism]
injm_sdpair1 [lemma, in gproduct]
injm_center [lemma, in center]
injm_quotm [lemma, in quotient]
Injm.aT [variable, in pgroup]
Injm.D [variable, in pgroup]
Injm.f [variable, in pgroup]
Injm.injf [variable, in pgroup]
Injm.rT [variable, in pgroup]
injm1 [lemma, in morphism]
injv [definition, in vector]
injvP [lemma, in vector]
inj_in_eq [lemma, in eqtype]
inj_eq [lemma, in eqtype]
inj_eqAxiom [lemma, in eqtype]
inj_id [lemma, in ssrfun]
inj_tperm [lemma, in perm]
inj_map [lemma, in seq]
inj_can_sym [lemma, in ssrfun]
inj_of_opair [definition, in choice]
inj_can_eq [lemma, in ssrfun]
inj_comp [lemma, in ssrfun]
InnerAutCyclicPgroup [section, in pgroup]
InnerAutCyclicPgroup.C [variable, in pgroup]
InnerAutCyclicPgroup.G [variable, in pgroup]
InnerAutCyclicPgroup.gT [variable, in pgroup]
InnerAutCyclicPgroup.nCG [variable, in pgroup]
InnerAutCyclicPgroup.p [variable, in pgroup]
innew [definition, in eqtype]
innew_val [lemma, in eqtype]
inord [definition, in fintype]
inordK [lemma, in fintype]
inord_val [lemma, in fintype]
inPhantom [definition, in ssrbool]
insigd [definition, in eqtype]
insT [definition, in seq]
insT [definition, in seq]
insub [definition, in eqtype]
insubd [definition, in eqtype]
insubdK [lemma, in eqtype]
insubF [lemma, in eqtype]
insubK [lemma, in eqtype]
insubN [lemma, in eqtype]
InsubNone [constructor, in eqtype]
insubP [lemma, in eqtype]
InsubSome [constructor, in eqtype]
insubT [lemma, in eqtype]
insub_eq [definition, in eqtype]
insub_spec [inductive, in eqtype]
insub_eqE [lemma, in eqtype]
IntegralDomain [module, in ssralg]
IntegralDomain [module, in finalg]
InternalAction [section, in hall]
InternalActionDefs [section, in action]
InternalActionDefs.gT [variable, in action]
InternalAction.gT [variable, in hall]
InternalAction.pi [variable, in hall]
InternalGroupAction [section, in action]
InternalGroupAction.CardClass [section, in action]
InternalGroupAction.CardClass.G [variable, in action]
InternalGroupAction.gT [variable, in action]
InternalProd [section, in gproduct]
InternalProd.DisjointRem [section, in gproduct]
InternalProd.DisjointRem.H [variable, in gproduct]
InternalProd.DisjointRem.K [variable, in gproduct]
InternalProd.DisjointRem.tiKH [variable, in gproduct]
InternalProd.gT [variable, in gproduct]
InternalProd.NormalComplement [section, in gproduct]
InternalProd.NormalComplement.complH_K [variable, in gproduct]
InternalProd.NormalComplement.G [variable, in gproduct]
InternalProd.NormalComplement.H [variable, in gproduct]
InternalProd.NormalComplement.K [variable, in gproduct]
InternalProd.NormalComplement.nKG [variable, in gproduct]
introF [lemma, in ssrbool]
introFn [lemma, in ssrbool]
introN [lemma, in ssrbool]
introNf [lemma, in ssrbool]
introNTF [lemma, in ssrbool]
introP [lemma, in ssrbool]
introT [lemma, in ssrbool]
introTF [lemma, in ssrbool]
introTFn [lemma, in ssrbool]
introTn [lemma, in ssrbool]
intro_mxsemisimple [lemma, in mxrepresentation]
intro_unitmx [lemma, in matrix]
intro_isoGrp [lemma, in presentation]
intro_closed [lemma, in fingraph]
intro_adjunction [lemma, in fingraph]
inT_bij [lemma, in ssrbool]
invariant [definition, in eqtype]
invariant_inj [lemma, in eqtype]
invariant_factor [definition, in gseries]
invariant_comp [lemma, in eqtype]
invariant_subnormal [lemma, in gseries]
invCg [lemma, in fingroup]
invDg [lemma, in fingroup]
InverseMorphism [section, in morphism]
InverseMorphism.aT [variable, in morphism]
InverseMorphism.f [variable, in morphism]
InverseMorphism.G [variable, in morphism]
InverseMorphism.injf [variable, in morphism]
InverseMorphism.rT [variable, in morphism]
invF [definition, in fintype]
invF_f [lemma, in fintype]
invg [definition, in fingroup]
invGid [lemma, in fingroup]
invgK [lemma, in fingroup]
invg_lcoset [lemma, in fingroup]
invg_rcoset [lemma, in fingroup]
invg_comm [lemma, in fingroup]
invg_set1 [lemma, in fingroup]
invg_inj [lemma, in fingroup]
invg_expg [lemma, in fingroup]
invg1 [lemma, in fingroup]
invg2id [lemma, in fingroup]
invIg [lemma, in fingroup]
InvLinearApp [section, in vector]
InvLinearApp.K [variable, in vector]
InvLinearApp.V [variable, in vector]
InvLinearApp.W [variable, in vector]
invm [definition, in morphism]
invmE [lemma, in morphism]
invMG [lemma, in fingroup]
invMg [lemma, in fingroup]
invmK [lemma, in morphism]
invmx [definition, in matrix]
invmxK [lemma, in matrix]
invmx_out [lemma, in matrix]
invm_morphism [definition, in morphism]
invm_subker [lemma, in morphism]
Involutions [section, in ssrfun]
involutions_gen_dihedral [lemma, in extremal]
Involutions.A [variable, in ssrfun]
Involutions.f [variable, in ssrfun]
Involutions.Hf [variable, in ssrfun]
involutive [definition, in ssrfun]
InvQuotientSpec [constructor, in quotient]
invSg [lemma, in fingroup]
invUg [lemma, in fingroup]
inv_quotientN [lemma, in quotient]
inv_bij [lemma, in ssrfun]
inv_quotient_spec [inductive, in quotient]
inv_inj [lemma, in ssrfun]
inv_lapp [definition, in vector]
inv_lapp_def [lemma, in vector]
inv_lker0 [lemma, in vector]
inv_subG [lemma, in fingroup]
inv_eq [lemma, in eqtype]
inv_quotientS [lemma, in quotient]
inW_bij [lemma, in ssrbool]
inZp [definition, in zmodp]
in_cprod [definition, in center]
in_submodJ [lemma, in mxrepresentation]
in_factmod_module [lemma, in mxrepresentation]
in_factmod_eq0 [lemma, in mxrepresentation]
in_setU [lemma, in finset]
in_set [lemma, in finset]
in_setD1 [lemma, in finset]
in_factmod_linear [definition, in mxrepresentation]
in_submod_linear [definition, in mxrepresentation]
in_submodE [lemma, in mxrepresentation]
in_submod_eq0 [lemma, in mxrepresentation]
in_setX [lemma, in finset]
in_factmodE [lemma, in mxrepresentation]
in_setU1 [lemma, in finset]
in_setC [lemma, in finset]
in_group [definition, in fingroup]
in_factmodJ [lemma, in mxrepresentation]
in_cons [lemma, in seq]
in_set1 [lemma, in finset]
in_setT [lemma, in finset]
in_submod_module [lemma, in mxrepresentation]
in_mem [definition, in ssrbool]
in_setD [lemma, in finset]
in_iinv_f [lemma, in fintype]
in_factmodsK [lemma, in mxrepresentation]
in_submod [definition, in mxrepresentation]
in_simpl [lemma, in ssrbool]
in_factmod_addsK [lemma, in mxrepresentation]
in_nil [lemma, in seq]
in_setI [lemma, in finset]
in_cprodM [lemma, in center]
in_set2 [lemma, in finset]
in_set0 [lemma, in finset]
in_cprod_morphism [definition, in center]
in_factmodK [lemma, in mxrepresentation]
in_submodK [lemma, in mxrepresentation]
in_setC1 [lemma, in finset]
in_factmod [definition, in mxrepresentation]
in1T [lemma, in ssrbool]
in1W [lemma, in ssrbool]
in2T [lemma, in ssrbool]
in2W [lemma, in ssrbool]
in3T [lemma, in ssrbool]
in3W [lemma, in ssrbool]
iota [definition, in seq]
iota_tuple [definition, in tuple]
iota_addl [lemma, in seq]
iota_tupleP [lemma, in tuple]
iota_add [lemma, in seq]
iota_uniq [lemma, in seq]
IRing [section, in poly]
IRing.a [variable, in poly]
IRing.R [variable, in poly]
irreflexive [definition, in ssrbool]
irrType [definition, in mxrepresentation]
irr_comp [definition, in mxrepresentation]
irr_reprK [lemma, in mxrepresentation]
irr_modeM [lemma, in mxrepresentation]
irr_mode_neq0 [lemma, in mxrepresentation]
irr_modeV [lemma, in mxrepresentation]
irr_mx_sum [lemma, in mxrepresentation]
irr_mode1 [lemma, in mxrepresentation]
irr_comp_id [lemma, in mxrepresentation]
irr_repr [definition, in mxrepresentation]
irr_degree_gt0 [lemma, in mxrepresentation]
irr_degree [definition, in mxrepresentation]
irr_center_scalar [lemma, in mxrepresentation]
irr_mode [definition, in mxrepresentation]
irr_reprE [lemma, in mxrepresentation]
irr_comp'_op0 [lemma, in mxrepresentation]
irr_comp_envelop [lemma, in mxrepresentation]
irr_mode_unit [lemma, in mxrepresentation]
irr_comp_rsim [lemma, in mxrepresentation]
irr_degree_abelian [lemma, in mxrepresentation]
irr_degreeE [lemma, in mxrepresentation]
irr_mx_mult [lemma, in mxrepresentation]
irr_modeX [lemma, in mxrepresentation]
irr1_mode [lemma, in mxrepresentation]
irr1_rfix [lemma, in mxrepresentation]
irr1_repr [lemma, in mxrepresentation]
isgroupP [lemma, in fingroup]
isMem [definition, in ssrbool]
IsMxvecIndex [constructor, in matrix]
isob [abbreviation, in center]
IsoBoolEquiv [section, in morphism]
IsoBoolEquiv.G [variable, in morphism]
IsoBoolEquiv.gT [variable, in morphism]
IsoBoolEquiv.H [variable, in morphism]
IsoBoolEquiv.hT [variable, in morphism]
IsoBoolEquiv.K [variable, in morphism]
IsoBoolEquiv.kT [variable, in morphism]
IsoCyclic [section, in cyclic]
IsoCyclic.gT [variable, in cyclic]
IsoCyclic.rT [variable, in cyclic]
IsoFitting [section, in maximal]
IsoFitting.D [variable, in maximal]
IsoFitting.f [variable, in maximal]
IsoFitting.G [variable, in maximal]
IsoFitting.gT [variable, in maximal]
IsoFitting.rT [variable, in maximal]
IsoFunctorTheory [section, in gfunctor]
IsoFunctorTheory.F [variable, in gfunctor]
Isog [section, in pgroup]
isog [definition, in morphism]
IsogAbelem [section, in abelian]
IsogAbelem.aT [variable, in abelian]
IsogAbelem.G [variable, in abelian]
IsogAbelem.H [variable, in abelian]
IsogAbelem.isoGH [variable, in abelian]
IsogAbelem.rT [variable, in abelian]
IsogAbelian [section, in abelian]
IsogAbelian.aT [variable, in abelian]
IsogAbelian.D [variable, in abelian]
IsogAbelian.f [variable, in abelian]
IsogAbelian.rT [variable, in abelian]
isogEcard [lemma, in morphism]
isogEhom [lemma, in morphism]
isogP [lemma, in morphism]
isoGrpP [lemma, in presentation]
isoGrp_hom [lemma, in presentation]
isoGrp_trans [lemma, in presentation]
isog_abelian_type [lemma, in abelian]
isog_transr [lemma, in morphism]
isog_cyclic_card [lemma, in cyclic]
isog_Mho [lemma, in abelian]
isog_simple [lemma, in gseries]
isog_Ohm [lemma, in abelian]
isog_2X1p2 [lemma, in extraspecial]
isog_sym [lemma, in morphism]
isog_abelian [lemma, in morphism]
isog_abelem_rV [lemma, in mxabelem]
isog_Fitting [lemma, in maximal]
isog_pX1p2 [lemma, in extraspecial]
isog_trans [lemma, in morphism]
isog_cprod_by [lemma, in center]
isog_nil_class [lemma, in nilpotent]
isog_symr [lemma, in morphism]
isog_abelem_card [lemma, in abelian]
isog_dprod [lemma, in gproduct]
isog_extraspecial [lemma, in maximal]
isog_transl [lemma, in morphism]
isog_xcprod [lemma, in center]
isog_set1X [lemma, in gproduct]
isog_pX1p2n [lemma, in extraspecial]
isog_refl [lemma, in morphism]
isog_pcore [lemma, in pgroup]
isog_abelem [lemma, in abelian]
isog_p_rank [lemma, in abelian]
isog_setX1 [lemma, in gproduct]
isog_pgroup [lemma, in pgroup]
isog_sol [lemma, in nilpotent]
isog_pseries [lemma, in pgroup]
isog_2extraspecial [lemma, in extraspecial]
isog_rank [lemma, in abelian]
isog_cyclic [lemma, in cyclic]
isog_center [lemma, in center]
isog_subg [lemma, in morphism]
isog_special [lemma, in maximal]
isog_hom [lemma, in morphism]
isog_eq1 [lemma, in morphism]
isog_grank [lemma, in abelian]
isog_nil [lemma, in nilpotent]
isog_Phi [lemma, in maximal]
isog_der [lemma, in commutator]
Isog.aT [variable, in pgroup]
Isog.G [variable, in pgroup]
Isog.H [variable, in pgroup]
Isog.rT [variable, in pgroup]
isom [definition, in morphism]
Isomorphisms [section, in morphism]
Isomorphisms.G [variable, in morphism]
Isomorphisms.gT [variable, in morphism]
Isomorphisms.H [variable, in morphism]
Isomorphisms.hT [variable, in morphism]
Isomorphisms.K [variable, in morphism]
Isomorphisms.kT [variable, in morphism]
isomP [lemma, in morphism]
isom_sgval [lemma, in morphism]
isom_card [lemma, in morphism]
isom_isog [lemma, in morphism]
isom_subg [lemma, in morphism]
isom_restr_perm [lemma, in action]
iso_u [definition, in mxrepresentation]
isSome [definition, in ssrbool]
isSome_insub [lemma, in eqtype]
isT [definition, in ssrbool]
is_span_seq1 [lemma, in vector]
is_perm_mxP [lemma, in matrix]
is_perm_mx [definition, in matrix]
is_abelem [definition, in abelian]
is_basis_notin0 [lemma, in vector]
is_span_span [lemma, in vector]
is_basis_span [lemma, in vector]
is_perm_mxMl [lemma, in matrix]
is_true_locked_true [lemma, in ssrbool]
is_span [definition, in vector]
is_basis_nil [lemma, in vector]
is_groupAction [definition, in action]
is_basis_vbasis [lemma, in vector]
is_scalar_mx [definition, in matrix]
is_scalar_mxP [lemma, in matrix]
is_basis [definition, in vector]
is_basis_free [lemma, in vector]
is_perm_mx1 [lemma, in matrix]
is_perm_mxMr [lemma, in matrix]
is_perm_mx_tr [lemma, in matrix]
is_perm_mxV [lemma, in matrix]
is_abelemP [lemma, in abelian]
is_total_action [lemma, in action]
is_abelem_pgroup [lemma, in abelian]
is_mxvec_index [inductive, in matrix]
is_action [definition, in action]
is_true_true [lemma, in ssrbool]
is_inleft [definition, in ssrbool]
is_left [definition, in ssrbool]
is_inl [definition, in ssrbool]
is_true [definition, in ssrbool]
is_basis_seq1 [lemma, in vector]
is_span_nil [lemma, in vector]
iter [definition, in ssrnat]
Iteration [section, in ssrnat]
Iteration.T [variable, in ssrnat]
IterCprod [section, in center]
IterCprod.G [variable, in center]
IterCprod.gT [variable, in center]
iteri [definition, in ssrnat]
iteriS [lemma, in ssrnat]
iterop [definition, in ssrnat]
iteropS [lemma, in ssrnat]
iterS [lemma, in ssrnat]
iterSr [lemma, in ssrnat]
iter_finv [lemma, in fingraph]
iter_pcycle [lemma, in perm]
iter_findex [lemma, in fingraph]
iter_order [lemma, in fingraph]
iter_add [lemma, in ssrnat]
i0 [definition, 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)