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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |

## I

id [abbreviation, in ssrfun]idempotent [definition, in ssrfun]

IdentityMorphism [section, in morphisms]

IdentityMorphism.gT [variable, in morphisms]

idfun [definition, in ssrfun]

idm [definition, in morphisms]

idmxE [lemma, in matrix]

idm_morphism [definition, in morphisms]

idm_morphM [lemma, in morphisms]

IdomainType [abbreviation, in ssralg]

idomainType [abbreviation, in ssralg]

idP [lemma, in ssrbool]

idPn [lemma, in ssrbool]

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]

IfSpecFalse [constructor, in ssrbool]

IfSpecTrue [constructor, in ssrbool]

if_arg [lemma, in ssrbool]

if_expr [definition, in ssrbool]

if_neg [lemma, in ssrbool]

if_same [lemma, in ssrbool]

if_spec [inductive, in ssrbool]

iinv [definition, in fintype]

iinv_f [lemma, in fintype]

iinv_proof [lemma, in fintype]

Image [section, in fintype]

image [definition, in fintype]

imageP [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]

image_codom [lemma, in fintype]

image_f [lemma, in fintype]

image_iinv [lemma, in fintype]

image_pre [lemma, in fintype]

image_pred0 [lemma, in fintype]

implybE [lemma, in ssrbool]

implybF [lemma, in ssrbool]

implybN [lemma, in ssrbool]

implybT [lemma, in ssrbool]

implyFb [lemma, in ssrbool]

implyP [lemma, in ssrbool]

implyTb [lemma, in ssrbool]

imset [abbreviation, in finset]

Imset [module, 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.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_def [abbreviation, in finset]

imset2_pair [lemma, in finset]

imset2_set1l [lemma, in finset]

imset2_set1r [lemma, in finset]

imset2_spec [inductive, in finset]

imset2_unlock [definition, in finset]

imset_autE [lemma, in automorphism]

imset_card [lemma, in finset]

imset_comp [lemma, in finset]

imset_coset [lemma, in normal]

imset_def [abbreviation, in finset]

imset_proper [lemma, in finset]

imset_set1 [lemma, in finset]

imset_unlock [definition, in finset]

inA_bij [lemma, in ssrbool]

incr_nth [definition, in seq]

index [definition, in seq]

indexg [definition, in groups]

indexgg [lemma, in groups]

indexgI [lemma, in groups]

indexgS [lemma, in groups]

indexg1 [lemma, in groups]

indexg_gt0 [lemma, in groups]

indexJg [lemma, in groups]

indexSg [lemma, in groups]

index1g [lemma, in groups]

index_cat [lemma, in seq]

index_cosetpre [lemma, in normal]

index_enum [definition, in bigops]

index_enum_ord [lemma, in fintype]

index_head [lemma, in seq]

index_injm [lemma, in normal]

index_iota [definition, in bigops]

index_last [lemma, in seq]

index_map [lemma, in seq]

index_mem [lemma, in seq]

index_morphim [lemma, in normal]

index_morphim_ker [lemma, in normal]

index_morphpre [lemma, in normal]

index_quotient [lemma, in normal]

index_quotient_eq [lemma, in normal]

index_quotient_ker [lemma, in normal]

index_size [lemma, in seq]

index_uniq [lemma, in seq]

inE [definition, in finset]

inE [definition, in ssrbool]

inE [definition, in seq]

inE [definition, in seq]

InheritedClasses [section, in groups]

InheritedClasses.T [variable, in groups]

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]

injF_bij [lemma, in fintype]

injF_codom [lemma, in fintype]

injmI [lemma, in morphisms]

injmK [lemma, in morphisms]

injmP [lemma, in morphisms]

injmSK [lemma, in morphisms]

injm1 [lemma, in morphisms]

injm_abelian [lemma, in morphisms]

injm_autm [lemma, in automorphism]

injm_cent [lemma, in morphisms]

injm_cent1 [lemma, in morphisms]

injm_comp [lemma, in morphisms]

injm_conj [lemma, in automorphism]

injm_cyclem [lemma, in cyclic]

injm_cyclic [lemma, in cyclic]

injm_factm [lemma, in morphisms]

injm_factmP [lemma, in morphisms]

injm_generator [lemma, in cyclic]

injm_idm [lemma, in morphisms]

injm_invm [lemma, in morphisms]

injm_norm [lemma, in morphisms]

injm_quotm [lemma, in normal]

injm_restrm [lemma, in morphisms]

injm_sgval [lemma, in morphisms]

injm_subcent [lemma, in morphisms]

injm_subcent1 [lemma, in morphisms]

injm_subg [lemma, in morphisms]

injm_subnorm [lemma, in morphisms]

injm_Zpm [lemma, in cyclic]

injm_Zp_unitm [lemma, in cyclic]

inj_can_eq [lemma, in ssrfun]

inj_can_sym [lemma, in ssrfun]

inj_comp [lemma, in ssrfun]

inj_eq [lemma, in eqtype]

inj_eqAxiom [lemma, in eqtype]

inj_id [lemma, in ssrfun]

inj_map [lemma, in seq]

inj_tperm [lemma, in perm]

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_eqE [lemma, in eqtype]

insub_spec [inductive, in eqtype]

IntegralDomain [module, in ssralg]

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_adjunction [lemma, in connect]

intro_closed [lemma, in connect]

intro_unit_mx [lemma, in matrix]

invariant [definition, in eqtype]

invariant_comp [lemma, in eqtype]

invariant_inj [lemma, in eqtype]

invCg [lemma, in groups]

invDg [lemma, in groups]

InverseMorphism [section, in morphisms]

InverseMorphism.aT [variable, in morphisms]

InverseMorphism.f [variable, in morphisms]

InverseMorphism.G [variable, in morphisms]

InverseMorphism.injf [variable, in morphisms]

InverseMorphism.rT [variable, in morphisms]

invF [definition, in fintype]

invF_f [lemma, in fintype]

invg [definition, in groups]

invGid [lemma, in groups]

invgK [lemma, in groups]

invg1 [lemma, in groups]

invg_comm [lemma, in groups]

invg_expg [lemma, in groups]

invg_inj [lemma, in groups]

invg_lcoset [lemma, in groups]

invg_rcoset [lemma, in groups]

invg_set1 [lemma, in groups]

invIg [lemma, in groups]

invm [definition, in morphisms]

invmE [lemma, in morphisms]

invMG [lemma, in groups]

invMg [lemma, in groups]

invmK [lemma, in morphisms]

invmx [definition, in matrix]

invmx_out [lemma, in matrix]

invm_dom [lemma, in morphisms]

invm_morphism [definition, in morphisms]

invm_subker [lemma, in morphisms]

Involutions [section, in ssrfun]

Involutions.A [variable, in ssrfun]

Involutions.f [variable, in ssrfun]

Involutions.Hf [variable, in ssrfun]

involutive [definition, in ssrfun]

InvQuotientSpec [constructor, in normal]

invSg [lemma, in groups]

invUg [lemma, in groups]

inv_bij [lemma, in ssrfun]

inv_eq [lemma, in eqtype]

inv_inj [lemma, in ssrfun]

inv_quotientN [lemma, in normal]

inv_quotientS [lemma, in normal]

inv_quotient_spec [inductive, in normal]

inv_subG [lemma, in groups]

inW_bij [lemma, in ssrbool]

inZp [definition, in zmodp]

in1A [lemma, in ssrbool]

in1W [lemma, in ssrbool]

in2A [lemma, in ssrbool]

in2W [lemma, in ssrbool]

in3A [lemma, in ssrbool]

in3W [lemma, in ssrbool]

in_cons [lemma, in seq]

in_group [definition, in groups]

in_iinv_f [lemma, in fintype]

in_mem [definition, in ssrbool]

in_nil [lemma, in seq]

in_set [lemma, in finset]

in_setC [lemma, in finset]

in_setC1 [lemma, in finset]

in_setD [lemma, in finset]

in_setD1 [lemma, in finset]

in_setI [lemma, in finset]

in_setT [lemma, in finset]

in_setU [lemma, in finset]

in_setU1 [lemma, in finset]

in_setX [lemma, in finset]

in_set0 [lemma, in finset]

in_set1 [lemma, in finset]

in_set2 [lemma, in finset]

in_simpl [lemma, in ssrbool]

iota [definition, in seq]

iota_add [lemma, in seq]

iota_addl [lemma, in seq]

iota_tuple [definition, in tuple]

iota_tupleP [lemma, in tuple]

iota_uniq [lemma, in seq]

irreflexive [definition, in ssrbool]

isgroupP [lemma, in groups]

isMem [definition, in ssrbool]

IsoBoolEquiv [section, in morphisms]

IsoBoolEquiv.G [variable, in morphisms]

IsoBoolEquiv.gT [variable, in morphisms]

IsoBoolEquiv.H [variable, in morphisms]

IsoBoolEquiv.hT [variable, in morphisms]

IsoBoolEquiv.K [variable, in morphisms]

IsoBoolEquiv.kT [variable, in morphisms]

IsoCyclic [section, in cyclic]

IsoCyclic.gT [variable, in cyclic]

IsoCyclic.rT [variable, in cyclic]

isog [definition, in morphisms]

isogP [lemma, in morphisms]

isog_abelian [lemma, in morphisms]

isog_card [lemma, in morphisms]

isog_cyclic [lemma, in cyclic]

isog_cyclic_card [lemma, in cyclic]

isog_refl [lemma, in morphisms]

isog_subg [lemma, in morphisms]

isog_sym [lemma, in morphisms]

isog_symr [lemma, in morphisms]

isog_trans [lemma, in morphisms]

isog_transl [lemma, in morphisms]

isog_transr [lemma, in morphisms]

isog_triv [lemma, in morphisms]

isom [definition, in morphisms]

Isomorphisms [section, in morphisms]

Isomorphisms.G [variable, in morphisms]

Isomorphisms.gT [variable, in morphisms]

Isomorphisms.H [variable, in morphisms]

Isomorphisms.hT [variable, in morphisms]

Isomorphisms.K [variable, in morphisms]

Isomorphisms.kT [variable, in morphisms]

isomP [lemma, in morphisms]

isom_card [lemma, in morphisms]

isom_isog [lemma, in morphisms]

isom_sgval [lemma, in morphisms]

isom_subg [lemma, in morphisms]

isSome [definition, in ssrbool]

isSome_insub [lemma, in eqtype]

is_inl [definition, in ssrbool]

is_inleft [definition, in ssrbool]

is_left [definition, in ssrbool]

is_perm_mx [definition, in matrix]

is_perm_mxMl [lemma, in matrix]

is_perm_mxMr [lemma, in matrix]

is_perm_mxP [lemma, in matrix]

is_perm_mxV [lemma, in matrix]

is_perm_mx1 [lemma, in matrix]

is_true [definition, in ssrbool]

is_true_locked_true [lemma, in ssrbool]

is_true_true [lemma, in ssrbool]

iter [definition, in ssrnat]

Iteration [section, in ssrnat]

Iteration.T [variable, in ssrnat]

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_add [lemma, in ssrnat]

iter_findex [lemma, in connect]

iter_finv [lemma, in connect]

iter_order [lemma, in connect]

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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |