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

idGfun_cont [in gfunctor]
idGfun_monotonic [in gfunctor]
idGfun_closed [in gfunctor]
idmxE [in matrix]
idm_morphM [in morphism]
idP [in ssrbool]
idPn [in ssrbool]
ifactmE [in morphism]
ifE [in ssrbool]
iffLR [in ssreflect]
iffLRn [in ssreflect]
iffP [in ssrbool]
iffRL [in ssreflect]
iffRLn [in ssreflect]
ifnE [in ssrnat]
ifnzP [in prime]
ifP [in ssrbool]
ifPn [in ssrbool]
if_arg [in ssrbool]
if_same [in ssrbool]
if_neg [in ssrbool]
iinv_proof [in fintype]
iinv_f [in fintype]
imageP [in fintype]
image_pred0 [in fintype]
image_injP [in fintype]
image_f [in fintype]
image_iinv [in fintype]
image_pre [in fintype]
image_codom [in fintype]
implybb [in ssrbool]
implybE [in ssrbool]
implybF [in ssrbool]
implybN [in ssrbool]
implybNN [in ssrbool]
implybT [in ssrbool]
implyb_idr [in ssrbool]
implyb_idl [in ssrbool]
implyb_id2l [in ssrbool]
implyFb [in ssrbool]
implyNb [in ssrbool]
implyP [in ssrbool]
implyTb [in ssrbool]
imsetI [in finset]
imsetP [in finset]
imsetS [in finset]
imsetU [in finset]
imsetU1 [in finset]
imset_injP [in finset]
imset_card [in finset]
imset_mulgm [in gproduct]
imset_set1 [in finset]
imset_autE [in automorphism]
imset_coset [in quotient]
imset_comp [in finset]
imset_proper [in finset]
Imset.imsetE [in finset]
Imset.imset2E [in finset]
imset0 [in finset]
imset2P [in finset]
imset2S [in finset]
imset2Sl [in finset]
imset2Sr [in finset]
imset2Ul [in finset]
imset2Ur [in finset]
imset2_set1r [in finset]
imset2_set1l [in finset]
imset2_pair [in finset]
im_conjgm_norm [in automorphism]
im_cyclem [in cyclic]
im_restr_perm [in action]
im_xcprodml [in center]
im_qisom [in quotient]
im_sdpair_norm [in gproduct]
im_sdpair_TI [in gproduct]
im_actperm_Aut [in action]
im_cpair [in center]
im_xcprodm [in center]
im_cpair_cent [in center]
im_rcosets_pcycle_transversal [in finmodule]
im_abelem_rV [in mxabelem]
im_subg [in morphism]
im_Aut_isom [in automorphism]
im_rVabelem [in mxabelem]
im_coset [in quotient]
im_sdpair [in gproduct]
im_cprodm [in gproduct]
im_permV [in perm]
im_sdprodm [in gproduct]
im_invm [in morphism]
im_eltm [in cyclic]
im_ifactm [in morphism]
im_xcprodmr [in center]
im_dprodm [in gproduct]
im_Zpm [in cyclic]
im_xsdprodm [in gproduct]
im_perm_on [in perm]
im_autm [in automorphism]
im_cpair_cprod [in center]
im_restrm [in morphism]
im_sgval [in morphism]
im_qisom_proof [in quotient]
im_actm [in action]
im_sdprodm2 [in gproduct]
im_idm [in morphism]
im_sdprodm1 [in gproduct]
im_Zp_unitm [in cyclic]
indexgg [in fingroup]
indexgI [in fingroup]
indexgS [in fingroup]
indexg_gt1 [in fingroup]
indexg_eq1 [in fingroup]
indexg_gt0 [in fingroup]
indexg1 [in fingroup]
indexJg [in fingroup]
indexMg [in fingroup]
indexSg [in fingroup]
index_quotient_ker [in quotient]
index_quotient_eq [in quotient]
index_injm [in quotient]
index_cat [in seq]
index_morphim [in quotient]
index_size [in seq]
index_mem [in seq]
index_uniq [in seq]
index_head [in seq]
index_cent1 [in action]
index_enum_ord [in fintype]
index_last [in seq]
index_cosetpre [in quotient]
index_morphim_ker [in quotient]
index_morphpre [in quotient]
index_map [in seq]
index_quotient [in quotient]
index_maxnormal_sol_prime [in maximal]
index1g [in fingroup]
index2_normal [in fingroup]
injectiveP [in fintype]
injectivePn [in fintype]
injF_bij [in fintype]
injF_codom [in fintype]
injmF [in gfunctor]
injmF_sub [in gfunctor]
injmI [in morphism]
injmK [in morphism]
injmP [in morphism]
injmSK [in morphism]
injm_norm [in morphism]
injm_pElem [in abelian]
injm_special [in maximal]
injm_Aut_sub [in action]
injm_dprodm [in gproduct]
injm_nElem [in abelian]
injm_Zpm [in cyclic]
injm_pcore [in pgroup]
injm_sdprodm [in gproduct]
injm_grank [in abelian]
injm_extraspecial [in maximal]
injm_cpair1g [in center]
injm_subcent [in morphism]
injm_xcprodm [in center]
injm_comp [in morphism]
injm_pHall [in pgroup]
injm_abelian [in morphism]
injm_cpairg1 [in center]
injm_subnorm [in morphism]
injm_faithful [in action]
injm_conj [in automorphism]
injm_cent1 [in morphism]
injm_cprodm [in gproduct]
injm_pairg1 [in gproduct]
injm_cyclem [in cyclic]
injm_xsdprodm [in gproduct]
injm_pprodm [in gproduct]
injm_sgval [in morphism]
injm_maximal_eq [in gseries]
injm_pseries [in pgroup]
injm_dprod [in gproduct]
injm_eltm [in cyclic]
injm_generator [in cyclic]
injm_rank [in abelian]
injm_Ldiv [in abelian]
injm_invm [in morphism]
injm_pelt [in pgroup]
injm_Aut_isom [in automorphism]
injm_pmaxElem [in abelian]
injm_pgroup [in pgroup]
injm_subg [in morphism]
injm_factm [in morphism]
injm_abelem [in abelian]
injm_Aut_full [in action]
injm_sdprod [in gproduct]
injm_subcent1 [in morphism]
injm_factmP [in morphism]
injm_ifactm [in morphism]
injm_cyclic [in cyclic]
injm_Ohm [in abelian]
injm_cent [in morphism]
injm_qisom [in quotient]
injm_pnElem [in abelian]
injm_actm [in action]
injm_restrm [in morphism]
injm_p_rank [in abelian]
injm_autm [in automorphism]
injm_pair1g [in gproduct]
injm_nil [in nilpotent]
injm_Aut [in automorphism]
injm_Zp_unitm [in cyclic]
injm_sdpair2 [in gproduct]
injm_maximal [in gseries]
injm_ucn [in nilpotent]
injm_sol [in nilpotent]
injm_idm [in morphism]
injm_Phi [in maximal]
injm_proper [in morphism]
injm_Fitting [in maximal]
injm_morphim_inj [in morphism]
injm_char [in automorphism]
injm_sdpair1 [in gproduct]
injm_center [in center]
injm_quotm [in quotient]
injm1 [in morphism]
injvP [in vector]
inj_in_eq [in eqtype]
inj_eq [in eqtype]
inj_eqAxiom [in eqtype]
inj_id [in ssrfun]
inj_tperm [in perm]
inj_map [in seq]
inj_can_sym [in ssrfun]
inj_can_eq [in ssrfun]
inj_comp [in ssrfun]
innew_val [in eqtype]
inordK [in fintype]
inord_val [in fintype]
insubdK [in eqtype]
insubF [in eqtype]
insubK [in eqtype]
insubN [in eqtype]
insubP [in eqtype]
insubT [in eqtype]
insub_eqE [in eqtype]
introF [in ssrbool]
introFn [in ssrbool]
introN [in ssrbool]
introNf [in ssrbool]
introNTF [in ssrbool]
introP [in ssrbool]
introT [in ssrbool]
introTF [in ssrbool]
introTFn [in ssrbool]
introTn [in ssrbool]
intro_mxsemisimple [in mxrepresentation]
intro_unitmx [in matrix]
intro_isoGrp [in presentation]
intro_closed [in fingraph]
intro_adjunction [in fingraph]
inT_bij [in ssrbool]
invariant_inj [in eqtype]
invariant_comp [in eqtype]
invariant_subnormal [in gseries]
invCg [in fingroup]
invDg [in fingroup]
invF_f [in fintype]
invGid [in fingroup]
invgK [in fingroup]
invg_lcoset [in fingroup]
invg_rcoset [in fingroup]
invg_comm [in fingroup]
invg_set1 [in fingroup]
invg_inj [in fingroup]
invg_expg [in fingroup]
invg1 [in fingroup]
invg2id [in fingroup]
invIg [in fingroup]
invmE [in morphism]
invMG [in fingroup]
invMg [in fingroup]
invmK [in morphism]
invmxK [in matrix]
invmx_out [in matrix]
invm_subker [in morphism]
involutions_gen_dihedral [in extremal]
invSg [in fingroup]
invUg [in fingroup]
inv_quotientN [in quotient]
inv_bij [in ssrfun]
inv_inj [in ssrfun]
inv_lapp_def [in vector]
inv_lker0 [in vector]
inv_subG [in fingroup]
inv_eq [in eqtype]
inv_quotientS [in quotient]
inW_bij [in ssrbool]
in_submodJ [in mxrepresentation]
in_factmod_module [in mxrepresentation]
in_factmod_eq0 [in mxrepresentation]
in_setU [in finset]
in_set [in finset]
in_setD1 [in finset]
in_submodE [in mxrepresentation]
in_submod_eq0 [in mxrepresentation]
in_setX [in finset]
in_factmodE [in mxrepresentation]
in_setU1 [in finset]
in_setC [in finset]
in_factmodJ [in mxrepresentation]
in_cons [in seq]
in_set1 [in finset]
in_setT [in finset]
in_submod_module [in mxrepresentation]
in_setD [in finset]
in_iinv_f [in fintype]
in_factmodsK [in mxrepresentation]
in_simpl [in ssrbool]
in_factmod_addsK [in mxrepresentation]
in_nil [in seq]
in_setI [in finset]
in_cprodM [in center]
in_set2 [in finset]
in_set0 [in finset]
in_factmodK [in mxrepresentation]
in_submodK [in mxrepresentation]
in_setC1 [in finset]
in1T [in ssrbool]
in1W [in ssrbool]
in2T [in ssrbool]
in2W [in ssrbool]
in3T [in ssrbool]
in3W [in ssrbool]
iota_addl [in seq]
iota_tupleP [in tuple]
iota_add [in seq]
iota_uniq [in seq]
irr_reprK [in mxrepresentation]
irr_modeM [in mxrepresentation]
irr_mode_neq0 [in mxrepresentation]
irr_modeV [in mxrepresentation]
irr_mx_sum [in mxrepresentation]
irr_mode1 [in mxrepresentation]
irr_comp_id [in mxrepresentation]
irr_degree_gt0 [in mxrepresentation]
irr_center_scalar [in mxrepresentation]
irr_reprE [in mxrepresentation]
irr_comp'_op0 [in mxrepresentation]
irr_comp_envelop [in mxrepresentation]
irr_mode_unit [in mxrepresentation]
irr_comp_rsim [in mxrepresentation]
irr_degree_abelian [in mxrepresentation]
irr_degreeE [in mxrepresentation]
irr_mx_mult [in mxrepresentation]
irr_modeX [in mxrepresentation]
irr1_mode [in mxrepresentation]
irr1_rfix [in mxrepresentation]
irr1_repr [in mxrepresentation]
isgroupP [in fingroup]
isogEcard [in morphism]
isogEhom [in morphism]
isogP [in morphism]
isoGrpP [in presentation]
isoGrp_hom [in presentation]
isoGrp_trans [in presentation]
isog_abelian_type [in abelian]
isog_transr [in morphism]
isog_cyclic_card [in cyclic]
isog_Mho [in abelian]
isog_simple [in gseries]
isog_Ohm [in abelian]
isog_2X1p2 [in extraspecial]
isog_sym [in morphism]
isog_abelian [in morphism]
isog_abelem_rV [in mxabelem]
isog_Fitting [in maximal]
isog_pX1p2 [in extraspecial]
isog_trans [in morphism]
isog_cprod_by [in center]
isog_nil_class [in nilpotent]
isog_symr [in morphism]
isog_abelem_card [in abelian]
isog_dprod [in gproduct]
isog_extraspecial [in maximal]
isog_transl [in morphism]
isog_xcprod [in center]
isog_set1X [in gproduct]
isog_pX1p2n [in extraspecial]
isog_refl [in morphism]
isog_pcore [in pgroup]
isog_abelem [in abelian]
isog_p_rank [in abelian]
isog_setX1 [in gproduct]
isog_pgroup [in pgroup]
isog_sol [in nilpotent]
isog_pseries [in pgroup]
isog_2extraspecial [in extraspecial]
isog_rank [in abelian]
isog_cyclic [in cyclic]
isog_center [in center]
isog_subg [in morphism]
isog_special [in maximal]
isog_hom [in morphism]
isog_eq1 [in morphism]
isog_grank [in abelian]
isog_nil [in nilpotent]
isog_Phi [in maximal]
isog_der [in commutator]
isomP [in morphism]
isom_sgval [in morphism]
isom_card [in morphism]
isom_isog [in morphism]
isom_subg [in morphism]
isom_restr_perm [in action]
isSome_insub [in eqtype]
is_span_seq1 [in vector]
is_perm_mxP [in matrix]
is_basis_notin0 [in vector]
is_span_span [in vector]
is_basis_span [in vector]
is_perm_mxMl [in matrix]
is_true_locked_true [in ssrbool]
is_basis_nil [in vector]
is_basis_vbasis [in vector]
is_scalar_mxP [in matrix]
is_basis_free [in vector]
is_perm_mx1 [in matrix]
is_perm_mxMr [in matrix]
is_perm_mx_tr [in matrix]
is_perm_mxV [in matrix]
is_abelemP [in abelian]
is_total_action [in action]
is_abelem_pgroup [in abelian]
is_true_true [in ssrbool]
is_basis_seq1 [in vector]
is_span_nil [in vector]
iteriS [in ssrnat]
iteropS [in ssrnat]
iterS [in ssrnat]
iterSr [in ssrnat]
iter_finv [in fingraph]
iter_pcycle [in perm]
iter_findex [in fingraph]
iter_order [in fingraph]
iter_add [in ssrnat]



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)