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

idempotent [in ssrfun]
idfun [in ssrfun]
idGfun [in gfunctor]
idm [in morphism]
idm_morphism [in morphism]
ifactm [in morphism]
ifnz [in prime]
ifn_expr [in ssrnat]
if_expr [in ssrbool]
iinv [in fintype]
image [in fintype]
imprimitivity_system [in primitive_action]
imset_unlock [in finset]
Imset.imset [in finset]
Imset.imset2 [in finset]
imset2_unlock [in finset]
incr_nth [in seq]
index [in seq]
indexg [in fingroup]
index_extremal_group_type [in extremal]
index_iota [in bigop]
index_enum [in bigop]
inE [in seq]
inE [in finset]
inE [in ssrbool]
inE [in seq]
injA [in hall]
injective [in ssrfun]
injectiveb [in fintype]
InjEqMixin [in eqtype]
injG [in hall]
injgz [in center]
injH [in center]
injK [in center]
injv [in vector]
inj_of_opair [in choice]
innew [in eqtype]
inord [in fintype]
inPhantom [in ssrbool]
insigd [in eqtype]
insT [in seq]
insT [in seq]
insub [in eqtype]
insubd [in eqtype]
insub_eq [in eqtype]
invariant [in eqtype]
invariant_factor [in gseries]
invF [in fintype]
invg [in fingroup]
invm [in morphism]
invmx [in matrix]
invm_morphism [in morphism]
involutive [in ssrfun]
inv_lapp [in vector]
inZp [in zmodp]
in_cprod [in center]
in_factmod_linear [in mxrepresentation]
in_submod_linear [in mxrepresentation]
in_group [in fingroup]
in_mem [in ssrbool]
in_submod [in mxrepresentation]
in_cprod_morphism [in center]
in_factmod [in mxrepresentation]
iota [in seq]
iota_tuple [in tuple]
irreflexive [in ssrbool]
irrType [in mxrepresentation]
irr_comp [in mxrepresentation]
irr_repr [in mxrepresentation]
irr_degree [in mxrepresentation]
irr_mode [in mxrepresentation]
isMem [in ssrbool]
isog [in morphism]
isom [in morphism]
iso_u [in mxrepresentation]
isSome [in ssrbool]
isT [in ssrbool]
is_perm_mx [in matrix]
is_abelem [in abelian]
is_span [in vector]
is_groupAction [in action]
is_scalar_mx [in matrix]
is_basis [in vector]
is_action [in action]
is_inleft [in ssrbool]
is_left [in ssrbool]
is_inl [in ssrbool]
is_true [in ssrbool]
iter [in ssrnat]
iteri [in ssrnat]
iterop [in ssrnat]
i0 [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)