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) |