| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +
I
+iC [abbreviation, in mathcomp.character.character]+IdealDef [section, in mathcomp.algebra.ring_quotient]
+IdealDef.IdealTheory [section, in mathcomp.algebra.ring_quotient]
+IdealDef.IdealTheory.I [variable, in mathcomp.algebra.ring_quotient]
+IdealDef.IdealTheory.idealrI [variable, in mathcomp.algebra.ring_quotient]
+IdealDef.IdealTheory.kI [variable, in mathcomp.algebra.ring_quotient]
+IdealDef.IdealTheory.R [variable, in mathcomp.algebra.ring_quotient]
+IdealDef.PrimeIdealTheory [section, in mathcomp.algebra.ring_quotient]
+IdealDef.PrimeIdealTheory.I [variable, in mathcomp.algebra.ring_quotient]
+IdealDef.PrimeIdealTheory.kI [variable, in mathcomp.algebra.ring_quotient]
+IdealDef.PrimeIdealTheory.pidealrI [variable, in mathcomp.algebra.ring_quotient]
+IdealDef.PrimeIdealTheory.R [variable, in mathcomp.algebra.ring_quotient]
+idealMr [lemma, in mathcomp.algebra.ring_quotient]
+Idealr [definition, in mathcomp.algebra.ring_quotient]
+idealr [record, in mathcomp.algebra.ring_quotient]
+idealr_zmod [projection, in mathcomp.algebra.ring_quotient]
+idealr_closedB [lemma, in mathcomp.algebra.ring_quotient]
+idealr_closed_nontrivial [lemma, in mathcomp.algebra.ring_quotient]
+idealr_closed [definition, in mathcomp.algebra.ring_quotient]
+idealr0 [lemma, in mathcomp.algebra.ring_quotient]
+idealr1 [lemma, in mathcomp.algebra.ring_quotient]
+IdentityMorphism [section, in mathcomp.fingroup.morphism]
+IdentityMorphism.gT [variable, in mathcomp.fingroup.morphism]
+idGfun [definition, in mathcomp.solvable.gfunctor]
+idGfun_monotonic [lemma, in mathcomp.solvable.gfunctor]
+idGfun_cont [lemma, in mathcomp.solvable.gfunctor]
+idGfun_closed [lemma, in mathcomp.solvable.gfunctor]
+idm [definition, in mathcomp.fingroup.morphism]
+idmxE [lemma, in mathcomp.algebra.matrix]
+idm_isom [lemma, in mathcomp.fingroup.morphism]
+idm_morphM [lemma, in mathcomp.fingroup.morphism]
+id_lfunE [lemma, in mathcomp.algebra.vector]
+id_lfun [definition, in mathcomp.algebra.vector]
+id_is_ahom [lemma, in mathcomp.field.falgebra]
+id1 [definition, in mathcomp.solvable.burnside_app]
+id3 [definition, in mathcomp.solvable.burnside_app]
+ieexprIz [lemma, in mathcomp.algebra.ssrint]
+ifactm [definition, in mathcomp.fingroup.morphism]
+ifactmE [lemma, in mathcomp.fingroup.morphism]
+ifnz [definition, in mathcomp.ssreflect.prime]
+ifnzP [lemma, in mathcomp.ssreflect.prime]
+IfnzPos [constructor, in mathcomp.ssreflect.prime]
+IfnzZero [constructor, in mathcomp.ssreflect.prime]
+ifnz_spec [inductive, in mathcomp.ssreflect.prime]
+ifN_eqC [lemma, in mathcomp.ssreflect.eqtype]
+ifN_eq [lemma, in mathcomp.ssreflect.eqtype]
+iG [abbreviation, in mathcomp.character.mxrepresentation]
+iinv [definition, in mathcomp.ssreflect.fintype]
+iinv_f [lemma, in mathcomp.ssreflect.fintype]
+iinv_proof [lemma, in mathcomp.ssreflect.fintype]
+Iirr [abbreviation, in mathcomp.character.character]
+Iirr_cast [lemma, in mathcomp.character.character]
+Iirr1_neq0 [lemma, in mathcomp.character.character]
+Image [section, in mathcomp.ssreflect.fintype]
+image [abbreviation, in mathcomp.ssreflect.fintype]
+imageP [lemma, in mathcomp.ssreflect.fintype]
+image_injP [lemma, in mathcomp.ssreflect.fintype]
+image_pre [lemma, in mathcomp.ssreflect.fintype]
+image_iinv [lemma, in mathcomp.ssreflect.fintype]
+image_pred0 [lemma, in mathcomp.ssreflect.fintype]
+image_codom [lemma, in mathcomp.ssreflect.fintype]
+image_f [lemma, in mathcomp.ssreflect.fintype]
+image_mem [definition, in mathcomp.ssreflect.fintype]
+Image.f [variable, in mathcomp.ssreflect.fintype]
+Image.Injective [section, in mathcomp.ssreflect.fintype]
+Image.Injective.injf [variable, in mathcomp.ssreflect.fintype]
+Image.SizeImage [section, in mathcomp.ssreflect.fintype]
+Image.SizeImage.f [variable, in mathcomp.ssreflect.fintype]
+Image.SizeImage.T' [variable, in mathcomp.ssreflect.fintype]
+Image.T [variable, in mathcomp.ssreflect.fintype]
+Image.T' [variable, in mathcomp.ssreflect.fintype]
+ImaginaryMixin [abbreviation, in mathcomp.algebra.ssrnum]
+imprimitivity_system [definition, in mathcomp.solvable.primitive_action]
+imset [abbreviation, in mathcomp.ssreflect.finset]
+Imset [module, in mathcomp.ssreflect.finset]
+ImsetCurry [section, in mathcomp.ssreflect.finset]
+ImsetCurry.aT1 [variable, in mathcomp.ssreflect.finset]
+ImsetCurry.aT2 [variable, in mathcomp.ssreflect.finset]
+ImsetCurry.Curry [section, in mathcomp.ssreflect.finset]
+ImsetCurry.Curry.A1 [variable, in mathcomp.ssreflect.finset]
+ImsetCurry.Curry.A2 [variable, in mathcomp.ssreflect.finset]
+ImsetCurry.Curry.D1 [variable, in mathcomp.ssreflect.finset]
+ImsetCurry.Curry.D2 [variable, in mathcomp.ssreflect.finset]
+ImsetCurry.f [variable, in mathcomp.ssreflect.finset]
+ImsetCurry.rT [variable, in mathcomp.ssreflect.finset]
+imsetI [lemma, in mathcomp.ssreflect.finset]
+imsetP [lemma, in mathcomp.ssreflect.finset]
+imsetS [lemma, in mathcomp.ssreflect.finset]
+ImsetSig [module, in mathcomp.ssreflect.finset]
+ImsetSig.imset [axiom, in mathcomp.ssreflect.finset]
+ImsetSig.imsetE [axiom, in mathcomp.ssreflect.finset]
+ImsetSig.imset2 [axiom, in mathcomp.ssreflect.finset]
+ImsetSig.imset2E [axiom, in mathcomp.ssreflect.finset]
+imsetU [lemma, in mathcomp.ssreflect.finset]
+imsetU1 [lemma, in mathcomp.ssreflect.finset]
+imset_coset [lemma, in mathcomp.fingroup.quotient]
+imset_mulgm [lemma, in mathcomp.fingroup.gproduct]
+imset_autE [lemma, in mathcomp.fingroup.automorphism]
+imset_comp [lemma, in mathcomp.ssreflect.finset]
+imset_id [lemma, in mathcomp.ssreflect.finset]
+imset_injP [lemma, in mathcomp.ssreflect.finset]
+imset_card [lemma, in mathcomp.ssreflect.finset]
+imset_proper [lemma, in mathcomp.ssreflect.finset]
+imset_set1 [lemma, in mathcomp.ssreflect.finset]
+imset_eq0 [lemma, in mathcomp.ssreflect.finset]
+imset_def [abbreviation, in mathcomp.ssreflect.finset]
+Imset.imset [definition, in mathcomp.ssreflect.finset]
+Imset.imsetE [lemma, in mathcomp.ssreflect.finset]
+Imset.imset2 [definition, in mathcomp.ssreflect.finset]
+Imset.imset2E [lemma, in mathcomp.ssreflect.finset]
+imset0 [lemma, in mathcomp.ssreflect.finset]
+imset2 [abbreviation, in mathcomp.ssreflect.finset]
+imset2P [lemma, in mathcomp.ssreflect.finset]
+imset2S [lemma, in mathcomp.ssreflect.finset]
+imset2Sl [lemma, in mathcomp.ssreflect.finset]
+Imset2spec [constructor, in mathcomp.ssreflect.finset]
+imset2Sr [lemma, in mathcomp.ssreflect.finset]
+imset2Ul [lemma, in mathcomp.ssreflect.finset]
+imset2Ur [lemma, in mathcomp.ssreflect.finset]
+imset2_set1r [lemma, in mathcomp.ssreflect.finset]
+imset2_set1l [lemma, in mathcomp.ssreflect.finset]
+imset2_pair [lemma, in mathcomp.ssreflect.finset]
+imset2_spec [inductive, in mathcomp.ssreflect.finset]
+imset2_def [abbreviation, in mathcomp.ssreflect.finset]
+im_qisom [lemma, in mathcomp.fingroup.quotient]
+im_qisom_proof [lemma, in mathcomp.fingroup.quotient]
+im_quotient [lemma, in mathcomp.fingroup.quotient]
+im_coset [lemma, in mathcomp.fingroup.quotient]
+im_perm_on [lemma, in mathcomp.fingroup.perm]
+im_permV [lemma, in mathcomp.fingroup.perm]
+im_xsdprodm [lemma, in mathcomp.fingroup.gproduct]
+im_sdprodm2 [lemma, in mathcomp.fingroup.gproduct]
+im_sdprodm1 [lemma, in mathcomp.fingroup.gproduct]
+im_dprodm [lemma, in mathcomp.fingroup.gproduct]
+im_cprodm [lemma, in mathcomp.fingroup.gproduct]
+im_sdprodm [lemma, in mathcomp.fingroup.gproduct]
+im_sdpair [lemma, in mathcomp.fingroup.gproduct]
+im_sdpair_TI [lemma, in mathcomp.fingroup.gproduct]
+im_sdpair_norm [lemma, in mathcomp.fingroup.gproduct]
+im_Aut_isom [lemma, in mathcomp.fingroup.automorphism]
+im_autm [lemma, in mathcomp.fingroup.automorphism]
+im_cfclass_Iirr [lemma, in mathcomp.character.inertia]
+im_actm [lemma, in mathcomp.fingroup.action]
+im_actperm_Aut [lemma, in mathcomp.fingroup.action]
+im_restr_perm [lemma, in mathcomp.fingroup.action]
+im_rVabelem [lemma, in mathcomp.character.mxabelem]
+im_abelem_rV [lemma, in mathcomp.character.mxabelem]
+im_sgval [lemma, in mathcomp.fingroup.morphism]
+im_subg [lemma, in mathcomp.fingroup.morphism]
+im_ifactm [lemma, in mathcomp.fingroup.morphism]
+im_invm [lemma, in mathcomp.fingroup.morphism]
+im_restrm [lemma, in mathcomp.fingroup.morphism]
+im_idm [lemma, in mathcomp.fingroup.morphism]
+im_xcprodmr [lemma, in mathcomp.solvable.center]
+im_xcprodml [lemma, in mathcomp.solvable.center]
+im_xcprodm [lemma, in mathcomp.solvable.center]
+im_cpair_cprod [lemma, in mathcomp.solvable.center]
+im_cpair [lemma, in mathcomp.solvable.center]
+im_cpair_cent [lemma, in mathcomp.solvable.center]
+im_Zp_unitm [lemma, in mathcomp.solvable.cyclic]
+im_cyclem [lemma, in mathcomp.solvable.cyclic]
+im_eltm [lemma, in mathcomp.solvable.cyclic]
+im_Zpm [lemma, in mathcomp.solvable.cyclic]
+im_transversal_repr [lemma, in mathcomp.ssreflect.finset]
+inA [abbreviation, in mathcomp.solvable.hall]
+incr_nthC [lemma, in mathcomp.ssreflect.seq]
+incr_nth_inj [lemma, in mathcomp.ssreflect.seq]
+incr_nth [definition, in mathcomp.ssreflect.seq]
+index [definition, in mathcomp.ssreflect.seq]
+indexg [definition, in mathcomp.fingroup.fingroup]
+indexgg [lemma, in mathcomp.fingroup.fingroup]
+indexgI [lemma, in mathcomp.fingroup.fingroup]
+indexgS [lemma, in mathcomp.fingroup.fingroup]
+indexg_gt1 [lemma, in mathcomp.fingroup.fingroup]
+indexg_eq1 [lemma, in mathcomp.fingroup.fingroup]
+indexg_gt0 [lemma, in mathcomp.fingroup.fingroup]
+indexg1 [lemma, in mathcomp.fingroup.fingroup]
+indexJg [lemma, in mathcomp.fingroup.fingroup]
+indexMg [lemma, in mathcomp.fingroup.fingroup]
+indexSg [lemma, in mathcomp.fingroup.fingroup]
+index_support_dvd_degree [lemma, in mathcomp.character.integral_char]
+index_cosetpre [lemma, in mathcomp.fingroup.quotient]
+index_quotient_eq [lemma, in mathcomp.fingroup.quotient]
+index_quotient [lemma, in mathcomp.fingroup.quotient]
+index_quotient_ker [lemma, in mathcomp.fingroup.quotient]
+index_morphpre [lemma, in mathcomp.fingroup.quotient]
+index_injm [lemma, in mathcomp.fingroup.quotient]
+index_morphim [lemma, in mathcomp.fingroup.quotient]
+index_morphim_ker [lemma, in mathcomp.fingroup.quotient]
+index_sdprodr [lemma, in mathcomp.fingroup.gproduct]
+index_sdprod [lemma, in mathcomp.fingroup.gproduct]
+index_extremal_group_type [definition, in mathcomp.solvable.extremal]
+index_map [lemma, in mathcomp.ssreflect.seq]
+index_last [lemma, in mathcomp.ssreflect.seq]
+index_head [lemma, in mathcomp.ssreflect.seq]
+index_uniq [lemma, in mathcomp.ssreflect.seq]
+index_cat [lemma, in mathcomp.ssreflect.seq]
+index_mem [lemma, in mathcomp.ssreflect.seq]
+index_size [lemma, in mathcomp.ssreflect.seq]
+index_maxnormal_sol_prime [lemma, in mathcomp.solvable.maximal]
+index_enum_ord [lemma, in mathcomp.ssreflect.fintype]
+index_cent1 [lemma, in mathcomp.fingroup.action]
+index_enum [definition, in mathcomp.ssreflect.bigop]
+index_iota [definition, in mathcomp.ssreflect.bigop]
+index1g [lemma, in mathcomp.fingroup.fingroup]
+index2_normal [lemma, in mathcomp.fingroup.fingroup]
+indir_iso3l [definition, in mathcomp.solvable.burnside_app]
+Induced [section, in mathcomp.character.character]
+Induced [section, in mathcomp.character.classfun]
+Induced.Def [section, in mathcomp.character.classfun]
+Induced.Def.A [variable, in mathcomp.character.classfun]
+Induced.Def.B [variable, in mathcomp.character.classfun]
+Induced.G [variable, in mathcomp.character.character]
+Induced.G [variable, in mathcomp.character.classfun]
+Induced.gT [variable, in mathcomp.character.character]
+Induced.gT [variable, in mathcomp.character.classfun]
+Induced.H [variable, in mathcomp.character.character]
+Induced.H [variable, in mathcomp.character.classfun]
+Induced.K [variable, in mathcomp.character.classfun]
+'Ind[ _ ] (ring_scope) [notation, in mathcomp.character.classfun]
+'Ind[ _ , _ ] (ring_scope) [notation, in mathcomp.character.classfun]
+Ind_Iirr [definition, in mathcomp.character.character]
+Ind_irr_neq0 [lemma, in mathcomp.character.character]
+inE [definition, in mathcomp.ssreflect.seq]
+inE [definition, in mathcomp.ssreflect.finset]
+inertia [definition, in mathcomp.character.inertia]
+Inertia [section, in mathcomp.character.inertia]
+inertia [library]
+InertiaBigdprod [section, in mathcomp.character.inertia]
+InertiaBigdprod.A [variable, in mathcomp.character.inertia]
+InertiaBigdprod.ConjBig [section, in mathcomp.character.inertia]
+InertiaBigdprod.ConjBig.nAy [variable, in mathcomp.character.inertia]
+InertiaBigdprod.ConjBig.y [variable, in mathcomp.character.inertia]
+InertiaBigdprod.defG [variable, in mathcomp.character.inertia]
+InertiaBigdprod.G [variable, in mathcomp.character.inertia]
+InertiaBigdprod.gT [variable, in mathcomp.character.inertia]
+InertiaBigdprod.I [variable, in mathcomp.character.inertia]
+InertiaBigdprod.InertiaBig [section, in mathcomp.character.inertia]
+InertiaBigdprod.InertiaBig.L [variable, in mathcomp.character.inertia]
+InertiaBigdprod.InertiaBig.nAL [variable, in mathcomp.character.inertia]
+InertiaBigdprod.P [variable, in mathcomp.character.inertia]
+InertiaDprod [section, in mathcomp.character.inertia]
+InertiaDprod.G [variable, in mathcomp.character.inertia]
+InertiaDprod.gT [variable, in mathcomp.character.inertia]
+InertiaDprod.H [variable, in mathcomp.character.inertia]
+InertiaDprod.K [variable, in mathcomp.character.inertia]
+InertiaDprod.KxH [variable, in mathcomp.character.inertia]
+inertiaJ [lemma, in mathcomp.character.inertia]
+InertiaSdprod [section, in mathcomp.character.inertia]
+InertiaSdprod.defG [variable, in mathcomp.character.inertia]
+InertiaSdprod.G [variable, in mathcomp.character.inertia]
+InertiaSdprod.gT [variable, in mathcomp.character.inertia]
+InertiaSdprod.H [variable, in mathcomp.character.inertia]
+InertiaSdprod.K [variable, in mathcomp.character.inertia]
+inertia_Frobenius_ker [lemma, in mathcomp.character.inertia]
+inertia_bigdprod_irr [lemma, in mathcomp.character.inertia]
+inertia_bigdprod [lemma, in mathcomp.character.inertia]
+inertia_bigdprodi [lemma, in mathcomp.character.inertia]
+inertia_dprod_irr [lemma, in mathcomp.character.inertia]
+inertia_dprod [lemma, in mathcomp.character.inertia]
+inertia_dprodr [lemma, in mathcomp.character.inertia]
+inertia_dprodl [lemma, in mathcomp.character.inertia]
+inertia_sdprod [lemma, in mathcomp.character.inertia]
+inertia_quo [lemma, in mathcomp.character.inertia]
+inertia_mod_quo [lemma, in mathcomp.character.inertia]
+inertia_mod_pre [lemma, in mathcomp.character.inertia]
+inertia_isom [lemma, in mathcomp.character.inertia]
+inertia_morph_im [lemma, in mathcomp.character.inertia]
+inertia_morph_pre [lemma, in mathcomp.character.inertia]
+inertia_id [lemma, in mathcomp.character.inertia]
+inertia_irr0 [lemma, in mathcomp.character.inertia]
+inertia_irr_prime [lemma, in mathcomp.character.inertia]
+inertia_injective [lemma, in mathcomp.character.inertia]
+inertia_prod [lemma, in mathcomp.character.inertia]
+inertia_mul [lemma, in mathcomp.character.inertia]
+inertia_opp [lemma, in mathcomp.character.inertia]
+inertia_scale_nz [lemma, in mathcomp.character.inertia]
+inertia_scale [lemma, in mathcomp.character.inertia]
+inertia_sum [lemma, in mathcomp.character.inertia]
+inertia_add [lemma, in mathcomp.character.inertia]
+Inertia_sub [lemma, in mathcomp.character.inertia]
+inertia_valJ [lemma, in mathcomp.character.inertia]
+Inertia.G [variable, in mathcomp.character.inertia]
+Inertia.gT [variable, in mathcomp.character.inertia]
+Inertia.H [variable, in mathcomp.character.inertia]
+_ ^: _ (cfun_scope) [notation, in mathcomp.character.inertia]
+'I_ _ [ _ ] (Group_scope) [notation, in mathcomp.character.inertia]
+'I[ _ ] (Group_scope) [notation, in mathcomp.character.inertia]
+'I_ _ [ _ ] (group_scope) [notation, in mathcomp.character.inertia]
+'I[ _ ] (group_scope) [notation, in mathcomp.character.inertia]
+inertia0 [lemma, in mathcomp.character.inertia]
+Inertia1 [lemma, in mathcomp.character.inertia]
+inertia1 [lemma, in mathcomp.character.inertia]
+infE [abbreviation, in mathcomp.solvable.burnside_app]
+infH [abbreviation, in mathcomp.fingroup.action]
+InfinitePrimitiveElementTheorem [section, in mathcomp.field.separable]
+InfinitePrimitiveElementTheorem.F [variable, in mathcomp.field.separable]
+InfinitePrimitiveElementTheorem.inFz [variable, in mathcomp.field.separable]
+InfinitePrimitiveElementTheorem.iota [variable, in mathcomp.field.separable]
+InfinitePrimitiveElementTheorem.L [variable, in mathcomp.field.separable]
+InfinitePrimitiveElementTheorem.nz_p [variable, in mathcomp.field.separable]
+InfinitePrimitiveElementTheorem.p [variable, in mathcomp.field.separable]
+InfinitePrimitiveElementTheorem.px_0 [variable, in mathcomp.field.separable]
+InfinitePrimitiveElementTheorem.x [variable, in mathcomp.field.separable]
+InfinitePrimitiveElementTheorem.y [variable, in mathcomp.field.separable]
+_ ^ _ (ring_scope) [notation, in mathcomp.field.separable]
+inG [abbreviation, in mathcomp.solvable.hall]
+inH [abbreviation, in mathcomp.fingroup.action]
+inIntSpan [definition, in mathcomp.algebra.intdiv]
+injectiveb [definition, in mathcomp.ssreflect.fintype]
+Injectiveb [section, in mathcomp.ssreflect.fintype]
+Injectiveb.aT [variable, in mathcomp.ssreflect.fintype]
+Injectiveb.f [variable, in mathcomp.ssreflect.fintype]
+Injectiveb.rT [variable, in mathcomp.ssreflect.fintype]
+injectiveP [lemma, in mathcomp.ssreflect.fintype]
+injectivePn [lemma, in mathcomp.ssreflect.fintype]
+InjEqMixin [definition, in mathcomp.ssreflect.eqtype]
+InjFactm [section, in mathcomp.fingroup.morphism]
+InjFactm.aT [variable, in mathcomp.fingroup.morphism]
+InjFactm.D [variable, in mathcomp.fingroup.morphism]
+InjFactm.f [variable, in mathcomp.fingroup.morphism]
+InjFactm.g [variable, in mathcomp.fingroup.morphism]
+InjFactm.G [variable, in mathcomp.fingroup.morphism]
+InjFactm.gT [variable, in mathcomp.fingroup.morphism]
+InjFactm.injf [variable, in mathcomp.fingroup.morphism]
+InjFactm.rT [variable, in mathcomp.fingroup.morphism]
+injF_bij [lemma, in mathcomp.ssreflect.fintype]
+injF_onto [lemma, in mathcomp.ssreflect.fintype]
+Injm [section, in mathcomp.solvable.pgroup]
+InjmAbelem [section, in mathcomp.solvable.abelian]
+InjmAbelem.aT [variable, in mathcomp.solvable.abelian]
+InjmAbelem.D [variable, in mathcomp.solvable.abelian]
+InjmAbelem.defG [variable, in mathcomp.solvable.abelian]
+InjmAbelem.f [variable, in mathcomp.solvable.abelian]
+InjmAbelem.G [variable, in mathcomp.solvable.abelian]
+InjmAbelem.injf [variable, in mathcomp.solvable.abelian]
+InjmAbelem.rT [variable, in mathcomp.solvable.abelian]
+InjmAbelem.sGD [variable, in mathcomp.solvable.abelian]
+InjmAut [section, in mathcomp.fingroup.automorphism]
+InjmAutIn [section, in mathcomp.fingroup.action]
+InjmAutIn.D [variable, in mathcomp.fingroup.action]
+InjmAutIn.f [variable, in mathcomp.fingroup.action]
+InjmAutIn.G [variable, in mathcomp.fingroup.action]
+InjmAutIn.gT [variable, in mathcomp.fingroup.action]
+InjmAutIn.H [variable, in mathcomp.fingroup.action]
+InjmAutIn.injf [variable, in mathcomp.fingroup.action]
+InjmAutIn.rT [variable, in mathcomp.fingroup.action]
+InjmAutIn.sGD [variable, in mathcomp.fingroup.action]
+InjmAutIn.sHD [variable, in mathcomp.fingroup.action]
+InjmAutIn.sHG [variable, in mathcomp.fingroup.action]
+InjmAut.D [variable, in mathcomp.fingroup.automorphism]
+InjmAut.domG [variable, in mathcomp.fingroup.automorphism]
+InjmAut.f [variable, in mathcomp.fingroup.automorphism]
+InjmAut.G [variable, in mathcomp.fingroup.automorphism]
+InjmAut.gT [variable, in mathcomp.fingroup.automorphism]
+InjmAut.injf [variable, in mathcomp.fingroup.automorphism]
+InjmAut.rT [variable, in mathcomp.fingroup.automorphism]
+InjmAut.sGD [variable, in mathcomp.fingroup.automorphism]
+InjmChar [section, in mathcomp.fingroup.automorphism]
+InjmChar.aT [variable, in mathcomp.fingroup.automorphism]
+InjmChar.D [variable, in mathcomp.fingroup.automorphism]
+InjmChar.f [variable, in mathcomp.fingroup.automorphism]
+InjmChar.injf [variable, in mathcomp.fingroup.automorphism]
+InjmChar.rT [variable, in mathcomp.fingroup.automorphism]
+injmD1 [lemma, in mathcomp.fingroup.morphism]
+injmF [lemma, in mathcomp.solvable.gfunctor]
+InjmFrobenius [section, in mathcomp.solvable.frobenius]
+InjmFrobenius.D [variable, in mathcomp.solvable.frobenius]
+InjmFrobenius.f [variable, in mathcomp.solvable.frobenius]
+InjmFrobenius.G [variable, in mathcomp.solvable.frobenius]
+InjmFrobenius.gT [variable, in mathcomp.solvable.frobenius]
+InjmFrobenius.rT [variable, in mathcomp.solvable.frobenius]
+injmF_sub [lemma, in mathcomp.solvable.gfunctor]
+injmI [lemma, in mathcomp.fingroup.morphism]
+injmK [lemma, in mathcomp.fingroup.morphism]
+InjmMax [section, in mathcomp.solvable.gseries]
+InjmMax.D [variable, in mathcomp.solvable.gseries]
+InjmMax.dG [variable, in mathcomp.solvable.gseries]
+InjmMax.dL [variable, in mathcomp.solvable.gseries]
+InjmMax.dM [variable, in mathcomp.solvable.gseries]
+InjmMax.f [variable, in mathcomp.solvable.gseries]
+InjmMax.G [variable, in mathcomp.solvable.gseries]
+InjmMax.gT [variable, in mathcomp.solvable.gseries]
+InjmMax.injf [variable, in mathcomp.solvable.gseries]
+InjmMax.L [variable, in mathcomp.solvable.gseries]
+InjmMax.M [variable, in mathcomp.solvable.gseries]
+InjmMax.rT [variable, in mathcomp.solvable.gseries]
+injmP [lemma, in mathcomp.fingroup.morphism]
+injmSK [lemma, in mathcomp.fingroup.morphism]
+injm_pseries [lemma, in mathcomp.solvable.pgroup]
+injm_pcore [lemma, in mathcomp.solvable.pgroup]
+injm_pHall [lemma, in mathcomp.solvable.pgroup]
+injm_pelt [lemma, in mathcomp.solvable.pgroup]
+injm_pgroup [lemma, in mathcomp.solvable.pgroup]
+injm_qisom [lemma, in mathcomp.fingroup.quotient]
+injm_quotm [lemma, in mathcomp.fingroup.quotient]
+injm_Frobenius_group [lemma, in mathcomp.solvable.frobenius]
+injm_Frobenius_ker [lemma, in mathcomp.solvable.frobenius]
+injm_Frobenius [lemma, in mathcomp.solvable.frobenius]
+injm_Frobenius_compl [lemma, in mathcomp.solvable.frobenius]
+injm_xsdprodm [lemma, in mathcomp.fingroup.gproduct]
+injm_dprodm [lemma, in mathcomp.fingroup.gproduct]
+injm_cprodm [lemma, in mathcomp.fingroup.gproduct]
+injm_sdprodm [lemma, in mathcomp.fingroup.gproduct]
+injm_pprodm [lemma, in mathcomp.fingroup.gproduct]
+injm_sdpair2 [lemma, in mathcomp.fingroup.gproduct]
+injm_sdpair1 [lemma, in mathcomp.fingroup.gproduct]
+injm_pairg1 [lemma, in mathcomp.fingroup.gproduct]
+injm_pair1g [lemma, in mathcomp.fingroup.gproduct]
+injm_bigdprod [lemma, in mathcomp.fingroup.gproduct]
+injm_dprod [lemma, in mathcomp.fingroup.gproduct]
+injm_sdprod [lemma, in mathcomp.fingroup.gproduct]
+injm_char [lemma, in mathcomp.fingroup.automorphism]
+injm_conj [lemma, in mathcomp.fingroup.automorphism]
+injm_Aut [lemma, in mathcomp.fingroup.automorphism]
+injm_Aut_isom [lemma, in mathcomp.fingroup.automorphism]
+injm_autm [lemma, in mathcomp.fingroup.automorphism]
+injm_Ohm [lemma, in mathcomp.solvable.abelian]
+injm_rank [lemma, in mathcomp.solvable.abelian]
+injm_p_rank [lemma, in mathcomp.solvable.abelian]
+injm_grank [lemma, in mathcomp.solvable.abelian]
+injm_pmaxElem [lemma, in mathcomp.solvable.abelian]
+injm_nElem [lemma, in mathcomp.solvable.abelian]
+injm_pnElem [lemma, in mathcomp.solvable.abelian]
+injm_pElem [lemma, in mathcomp.solvable.abelian]
+injm_abelem [lemma, in mathcomp.solvable.abelian]
+injm_Ldiv [lemma, in mathcomp.solvable.abelian]
+injm_minnormal [lemma, in mathcomp.solvable.gseries]
+injm_maxnormal [lemma, in mathcomp.solvable.gseries]
+injm_maximal_eq [lemma, in mathcomp.solvable.gseries]
+injm_maximal [lemma, in mathcomp.solvable.gseries]
+injm_extraspecial [lemma, in mathcomp.solvable.maximal]
+injm_special [lemma, in mathcomp.solvable.maximal]
+injm_Fitting [lemma, in mathcomp.solvable.maximal]
+injm_Phi [lemma, in mathcomp.solvable.maximal]
+injm_actm [lemma, in mathcomp.fingroup.action]
+injm_Aut_full [lemma, in mathcomp.fingroup.action]
+injm_Aut_sub [lemma, in mathcomp.fingroup.action]
+injm_faithful [lemma, in mathcomp.fingroup.action]
+injm_sol [lemma, in mathcomp.solvable.nilpotent]
+injm_nil [lemma, in mathcomp.solvable.nilpotent]
+injm_ucn [lemma, in mathcomp.solvable.nilpotent]
+injm_subg [lemma, in mathcomp.fingroup.morphism]
+injm_sgval [lemma, in mathcomp.fingroup.morphism]
+injm_ifactm [lemma, in mathcomp.fingroup.morphism]
+injm_invm [lemma, in mathcomp.fingroup.morphism]
+injm_proper [lemma, in mathcomp.fingroup.morphism]
+injm_factmP [lemma, in mathcomp.fingroup.morphism]
+injm_factm [lemma, in mathcomp.fingroup.morphism]
+injm_comp [lemma, in mathcomp.fingroup.morphism]
+injm_restrm [lemma, in mathcomp.fingroup.morphism]
+injm_idm [lemma, in mathcomp.fingroup.morphism]
+injm_abelian [lemma, in mathcomp.fingroup.morphism]
+injm_subcent [lemma, in mathcomp.fingroup.morphism]
+injm_cents [lemma, in mathcomp.fingroup.morphism]
+injm_cent [lemma, in mathcomp.fingroup.morphism]
+injm_subcent1 [lemma, in mathcomp.fingroup.morphism]
+injm_cent1 [lemma, in mathcomp.fingroup.morphism]
+injm_subnorm [lemma, in mathcomp.fingroup.morphism]
+injm_normal [lemma, in mathcomp.fingroup.morphism]
+injm_norms [lemma, in mathcomp.fingroup.morphism]
+injm_norm [lemma, in mathcomp.fingroup.morphism]
+injm_eq [lemma, in mathcomp.fingroup.morphism]
+injm_morphim_inj [lemma, in mathcomp.fingroup.morphism]
+injm_xcprodm [lemma, in mathcomp.solvable.center]
+injm_cpair1g [lemma, in mathcomp.solvable.center]
+injm_cpairg1 [lemma, in mathcomp.solvable.center]
+injm_center [lemma, in mathcomp.solvable.center]
+injm_Zp_unitm [lemma, in mathcomp.solvable.cyclic]
+injm_cyclem [lemma, in mathcomp.solvable.cyclic]
+injm_generator [lemma, in mathcomp.solvable.cyclic]
+injm_cyclic [lemma, in mathcomp.solvable.cyclic]
+injm_eltm [lemma, in mathcomp.solvable.cyclic]
+injm_Zpm [lemma, in mathcomp.solvable.cyclic]
+Injm.aT [variable, in mathcomp.solvable.pgroup]
+Injm.D [variable, in mathcomp.solvable.pgroup]
+Injm.f [variable, in mathcomp.solvable.pgroup]
+Injm.injf [variable, in mathcomp.solvable.pgroup]
+Injm.rT [variable, in mathcomp.solvable.pgroup]
+injm1 [lemma, in mathcomp.fingroup.morphism]
+inj_subfx [definition, in mathcomp.field.fieldext]
+inj_tperm [lemma, in mathcomp.fingroup.perm]
+inj_map [lemma, in mathcomp.ssreflect.seq]
+inj_card_bij [lemma, in mathcomp.ssreflect.fintype]
+inj_card_onto [lemma, in mathcomp.ssreflect.fintype]
+inj_eqAxiom [lemma, in mathcomp.ssreflect.eqtype]
+inj_in_eq [lemma, in mathcomp.ssreflect.eqtype]
+inj_eq [lemma, in mathcomp.ssreflect.eqtype]
+inlined_new_rect [abbreviation, in mathcomp.ssreflect.eqtype]
+inlined_sub_rect [abbreviation, in mathcomp.ssreflect.eqtype]
+InnerAutCyclicPgroup [section, in mathcomp.solvable.pgroup]
+InnerAutCyclicPgroup.C [variable, in mathcomp.solvable.pgroup]
+InnerAutCyclicPgroup.G [variable, in mathcomp.solvable.pgroup]
+InnerAutCyclicPgroup.gT [variable, in mathcomp.solvable.pgroup]
+InnerAutCyclicPgroup.nCG [variable, in mathcomp.solvable.pgroup]
+InnerAutCyclicPgroup.p [variable, in mathcomp.solvable.pgroup]
+InnerProduct [section, in mathcomp.character.character]
+InnerProduct.G [variable, in mathcomp.character.character]
+InnerProduct.gT [variable, in mathcomp.character.character]
+innew [definition, in mathcomp.ssreflect.eqtype]
+innew_val [lemma, in mathcomp.ssreflect.eqtype]
+inord [definition, in mathcomp.ssreflect.fintype]
+inordK [lemma, in mathcomp.ssreflect.fintype]
+inord_val [lemma, in mathcomp.ssreflect.fintype]
+InPrealField [section, in mathcomp.algebra.rat]
+InPrealField.F [variable, in mathcomp.algebra.rat]
+InRing [section, in mathcomp.algebra.rat]
+InRing.R [variable, in mathcomp.algebra.rat]
+inseparable_sum [lemma, in mathcomp.field.separable]
+inseparable_add [lemma, in mathcomp.field.separable]
+insigd [definition, in mathcomp.ssreflect.eqtype]
+insub [definition, in mathcomp.ssreflect.eqtype]
+insubd [definition, in mathcomp.ssreflect.eqtype]
+insubdK [lemma, in mathcomp.ssreflect.eqtype]
+insubF [lemma, in mathcomp.ssreflect.eqtype]
+insubK [lemma, in mathcomp.ssreflect.eqtype]
+insubN [lemma, in mathcomp.ssreflect.eqtype]
+InsubNone [constructor, in mathcomp.ssreflect.eqtype]
+insubP [lemma, in mathcomp.ssreflect.eqtype]
+InsubSome [constructor, in mathcomp.ssreflect.eqtype]
+insubT [lemma, in mathcomp.ssreflect.eqtype]
+insub_eqE [lemma, in mathcomp.ssreflect.eqtype]
+insub_eq [definition, in mathcomp.ssreflect.eqtype]
+insub_spec [inductive, in mathcomp.ssreflect.eqtype]
+int [inductive, in mathcomp.algebra.ssrint]
+intCK [lemma, in mathcomp.field.algC]
+IntDist [module, in mathcomp.algebra.ssrint]
+IntDist.Distn [section, in mathcomp.algebra.ssrint]
+IntDist.distnC [lemma, in mathcomp.algebra.ssrint]
+IntDist.distnDl [lemma, in mathcomp.algebra.ssrint]
+IntDist.distnDr [lemma, in mathcomp.algebra.ssrint]
+IntDist.distnEl [lemma, in mathcomp.algebra.ssrint]
+IntDist.distnEr [lemma, in mathcomp.algebra.ssrint]
+IntDist.distnn [lemma, in mathcomp.algebra.ssrint]
+IntDist.distnS [lemma, in mathcomp.algebra.ssrint]
+IntDist.distn_eq1 [lemma, in mathcomp.algebra.ssrint]
+IntDist.distn_eq0 [lemma, in mathcomp.algebra.ssrint]
+IntDist.distn0 [lemma, in mathcomp.algebra.ssrint]
+IntDist.distSn [lemma, in mathcomp.algebra.ssrint]
+IntDist.dist0n [lemma, in mathcomp.algebra.ssrint]
+IntDist.leqif_add_dist [lemma, in mathcomp.algebra.ssrint]
+IntDist.leqif_add_distz [lemma, in mathcomp.algebra.ssrint]
+IntDist.leq_add_dist [lemma, in mathcomp.algebra.ssrint]
+IntDist.sqrn_dist [lemma, in mathcomp.algebra.ssrint]
+_ - _ (distn_scope) [notation, in mathcomp.algebra.ssrint]
+`| _ | (nat_scope) [notation, in mathcomp.algebra.ssrint]
+intdiv [library]
+IntegralChar [section, in mathcomp.character.integral_char]
+IntegralChar.G [variable, in mathcomp.character.integral_char]
+IntegralChar.GringIrrMode [section, in mathcomp.character.integral_char]
+IntegralChar.GringIrrMode.i [variable, in mathcomp.character.integral_char]
+IntegralChar.GringIrrMode.mxZn_inj [variable, in mathcomp.character.integral_char]
+IntegralChar.GringIrrMode.n [variable, in mathcomp.character.integral_char]
+IntegralChar.gT [variable, in mathcomp.character.integral_char]
+integralOver [definition, in mathcomp.algebra.mxpoly]
+IntegralOverComRing [section, in mathcomp.algebra.mxpoly]
+IntegralOverComRing.intR_XsubC [variable, in mathcomp.algebra.mxpoly]
+IntegralOverComRing.K [variable, in mathcomp.algebra.mxpoly]
+IntegralOverComRing.R [variable, in mathcomp.algebra.mxpoly]
+IntegralOverComRing.RtoK [variable, in mathcomp.algebra.mxpoly]
+IntegralOverComRing.XsubC0 [variable, in mathcomp.algebra.mxpoly]
+IntegralOverField [section, in mathcomp.algebra.mxpoly]
+IntegralOverField.E [variable, in mathcomp.algebra.mxpoly]
+IntegralOverField.F [variable, in mathcomp.algebra.mxpoly]
+IntegralOverField.FtoE [variable, in mathcomp.algebra.mxpoly]
+IntegralOverRing [section, in mathcomp.algebra.mxpoly]
+IntegralOverRing.B [variable, in mathcomp.algebra.mxpoly]
+IntegralOverRing.BtoR [variable, in mathcomp.algebra.mxpoly]
+IntegralOverRing.K [variable, in mathcomp.algebra.mxpoly]
+IntegralOverRing.R [variable, in mathcomp.algebra.mxpoly]
+IntegralOverRing.RtoK [variable, in mathcomp.algebra.mxpoly]
+integralRange [definition, in mathcomp.algebra.mxpoly]
+integral_root [lemma, in mathcomp.algebra.mxpoly]
+integral_div [lemma, in mathcomp.algebra.mxpoly]
+integral_inv [lemma, in mathcomp.algebra.mxpoly]
+integral_algebraic [lemma, in mathcomp.algebra.mxpoly]
+integral_mul [lemma, in mathcomp.algebra.mxpoly]
+integral_add [lemma, in mathcomp.algebra.mxpoly]
+integral_sub [lemma, in mathcomp.algebra.mxpoly]
+integral_horner [lemma, in mathcomp.algebra.mxpoly]
+integral_opp [lemma, in mathcomp.algebra.mxpoly]
+integral_root_monic [lemma, in mathcomp.algebra.mxpoly]
+integral_horner_root [lemma, in mathcomp.algebra.mxpoly]
+integral_poly [lemma, in mathcomp.algebra.mxpoly]
+integral_nat [lemma, in mathcomp.algebra.mxpoly]
+integral_id [lemma, in mathcomp.algebra.mxpoly]
+integral_rmorph [lemma, in mathcomp.algebra.mxpoly]
+integral_char [library]
+integral0 [lemma, in mathcomp.algebra.mxpoly]
+integral1 [lemma, in mathcomp.algebra.mxpoly]
+InternalAction [section, in mathcomp.solvable.hall]
+InternalActionDefs [section, in mathcomp.fingroup.action]
+InternalActionDefs.gT [variable, in mathcomp.fingroup.action]
+InternalAction.gT [variable, in mathcomp.solvable.hall]
+InternalAction.pi [variable, in mathcomp.solvable.hall]
+InternalGroupAction [section, in mathcomp.fingroup.action]
+InternalGroupAction.CardClass [section, in mathcomp.fingroup.action]
+InternalGroupAction.CardClass.G [variable, in mathcomp.fingroup.action]
+InternalGroupAction.gT [variable, in mathcomp.fingroup.action]
+InternalProd [section, in mathcomp.fingroup.gproduct]
+InternalProd.DisjointRem [section, in mathcomp.fingroup.gproduct]
+InternalProd.DisjointRem.H [variable, in mathcomp.fingroup.gproduct]
+InternalProd.DisjointRem.K [variable, in mathcomp.fingroup.gproduct]
+InternalProd.DisjointRem.tiKH [variable, in mathcomp.fingroup.gproduct]
+InternalProd.gT [variable, in mathcomp.fingroup.gproduct]
+InternalProd.NormalComplement [section, in mathcomp.fingroup.gproduct]
+InternalProd.NormalComplement.complH_K [variable, in mathcomp.fingroup.gproduct]
+InternalProd.NormalComplement.G [variable, in mathcomp.fingroup.gproduct]
+InternalProd.NormalComplement.H [variable, in mathcomp.fingroup.gproduct]
+InternalProd.NormalComplement.K [variable, in mathcomp.fingroup.gproduct]
+Interval [constructor, in mathcomp.algebra.interval]
+interval [inductive, in mathcomp.algebra.interval]
+interval [library]
+IntervalField [section, in mathcomp.algebra.interval]
+IntervalField.R [variable, in mathcomp.algebra.interval]
+IntervalOrdered [section, in mathcomp.algebra.interval]
+IntervalOrdered.R [variable, in mathcomp.algebra.interval]
+IntervalPo [section, in mathcomp.algebra.interval]
+IntervalPo.R [variable, in mathcomp.algebra.interval]
+_ <= _ ?< if _ (ring_scope) [notation, in mathcomp.algebra.interval]
+`] -oo , +oo [ (ring_scope) [notation, in mathcomp.algebra.interval]
+`] _ , +oo [ (ring_scope) [notation, in mathcomp.algebra.interval]
+`[ _ , +oo [ (ring_scope) [notation, in mathcomp.algebra.interval]
+`] -oo , _ [ (ring_scope) [notation, in mathcomp.algebra.interval]
+`] -oo , _ ] (ring_scope) [notation, in mathcomp.algebra.interval]
+`] _ , _ [ (ring_scope) [notation, in mathcomp.algebra.interval]
+`[ _ , _ [ (ring_scope) [notation, in mathcomp.algebra.interval]
+`] _ , _ ] (ring_scope) [notation, in mathcomp.algebra.interval]
+`[ _ , _ ] (ring_scope) [notation, in mathcomp.algebra.interval]
+intEsg [lemma, in mathcomp.algebra.ssrint]
+intEsign [lemma, in mathcomp.algebra.ssrint]
+intmul [definition, in mathcomp.algebra.ssrint]
+intmul1_is_rmorphism [lemma, in mathcomp.algebra.ssrint]
+intOrdered [module, in mathcomp.algebra.ssrint]
+intOrderedTheory [section, in mathcomp.algebra.ssrint]
+intOrdered.abszN [lemma, in mathcomp.algebra.ssrint]
+intOrdered.eq0_normz [lemma, in mathcomp.algebra.ssrint]
+intOrdered.intOrdered [section, in mathcomp.algebra.ssrint]
+intOrdered.lez [definition, in mathcomp.algebra.ssrint]
+intOrdered.lez_def [lemma, in mathcomp.algebra.ssrint]
+intOrdered.lez_total [lemma, in mathcomp.algebra.ssrint]
+intOrdered.lez_norm_add [lemma, in mathcomp.algebra.ssrint]
+intOrdered.ltz [definition, in mathcomp.algebra.ssrint]
+intOrdered.ltz_def [lemma, in mathcomp.algebra.ssrint]
+intOrdered.ltz_add [lemma, in mathcomp.algebra.ssrint]
+intOrdered.Mixin [definition, in mathcomp.algebra.ssrint]
+intOrdered.normz [abbreviation, in mathcomp.algebra.ssrint]
+intOrdered.normzM [lemma, in mathcomp.algebra.ssrint]
+intOrdered.subz_ge0 [lemma, in mathcomp.algebra.ssrint]
+intP [lemma, in mathcomp.algebra.ssrint]
+intq_eq0 [lemma, in mathcomp.algebra.rat]
+intr [abbreviation, in mathcomp.algebra.ssrint]
+intrD [lemma, in mathcomp.algebra.ssrint]
+intRing [module, in mathcomp.algebra.ssrint]
+intRingTheory [section, in mathcomp.algebra.ssrint]
+intRing.comMixin [definition, in mathcomp.algebra.ssrint]
+intRing.intRing [section, in mathcomp.algebra.ssrint]
+_ * _ (int_scope) [notation, in mathcomp.algebra.ssrint]
+*%Z (int_scope) [notation, in mathcomp.algebra.ssrint]
+1 (int_scope) [notation, in mathcomp.algebra.ssrint]
+intRing.mulNz [lemma, in mathcomp.algebra.ssrint]
+intRing.mulz [definition, in mathcomp.algebra.ssrint]
+intRing.mulzA [lemma, in mathcomp.algebra.ssrint]
+intRing.mulzC [lemma, in mathcomp.algebra.ssrint]
+intRing.mulzN [lemma, in mathcomp.algebra.ssrint]
+intRing.mulzS [lemma, in mathcomp.algebra.ssrint]
+intRing.mulz_addl [lemma, in mathcomp.algebra.ssrint]
+intRing.mulz0 [lemma, in mathcomp.algebra.ssrint]
+intRing.mul0z [lemma, in mathcomp.algebra.ssrint]
+intRing.mul1z [lemma, in mathcomp.algebra.ssrint]
+intRing.nonzero1z [lemma, in mathcomp.algebra.ssrint]
+intrM [lemma, in mathcomp.algebra.ssrint]
+intro_mxsemisimple [lemma, in mathcomp.character.mxrepresentation]
+intro_unitmx [lemma, in mathcomp.algebra.matrix]
+intro_isoGrp [lemma, in mathcomp.fingroup.presentation]
+intro_class_fun [lemma, in mathcomp.character.classfun]
+intro_adjunction [lemma, in mathcomp.ssreflect.fingraph]
+intro_closed [lemma, in mathcomp.ssreflect.fingraph]
+intrp [abbreviation, in mathcomp.field.algC]
+intrp [abbreviation, in mathcomp.field.cyclotomic]
+intrp [abbreviation, in mathcomp.field.algnum]
+intrV [lemma, in mathcomp.algebra.ssrint]
+intr_norm [lemma, in mathcomp.algebra.ssrint]
+intr_sign [lemma, in mathcomp.algebra.ssrint]
+intr_sg [lemma, in mathcomp.algebra.ssrint]
+intr_inj [definition, in mathcomp.algebra.ssrint]
+intr_eq0 [lemma, in mathcomp.algebra.ssrint]
+intS [lemma, in mathcomp.algebra.ssrint]
+intUnitRing [module, in mathcomp.algebra.ssrint]
+intUnitRing.comMixin [definition, in mathcomp.algebra.ssrint]
+intUnitRing.idomain_axiomz [lemma, in mathcomp.algebra.ssrint]
+intUnitRing.intUnitRing [section, in mathcomp.algebra.ssrint]
+intUnitRing.invz [definition, in mathcomp.algebra.ssrint]
+intUnitRing.invz_out [lemma, in mathcomp.algebra.ssrint]
+intUnitRing.mulVz [lemma, in mathcomp.algebra.ssrint]
+intUnitRing.mulzn_eq1 [lemma, in mathcomp.algebra.ssrint]
+intUnitRing.unitz [definition, in mathcomp.algebra.ssrint]
+intUnitRing.unitzPl [lemma, in mathcomp.algebra.ssrint]
+intz [lemma, in mathcomp.algebra.ssrint]
+intZmod [module, in mathcomp.algebra.ssrint]
+intZmoduleTheory [section, in mathcomp.algebra.ssrint]
+intZmod.addNz [lemma, in mathcomp.algebra.ssrint]
+intZmod.addPz [lemma, in mathcomp.algebra.ssrint]
+intZmod.addSnz [lemma, in mathcomp.algebra.ssrint]
+intZmod.addSz [lemma, in mathcomp.algebra.ssrint]
+intZmod.addz [definition, in mathcomp.algebra.ssrint]
+intZmod.addzA [lemma, in mathcomp.algebra.ssrint]
+intZmod.addzC [lemma, in mathcomp.algebra.ssrint]
+intZmod.add0z [lemma, in mathcomp.algebra.ssrint]
+intZmod.add1Pz [lemma, in mathcomp.algebra.ssrint]
+intZmod.intP [lemma, in mathcomp.algebra.ssrint]
+intZmod.intZmod [section, in mathcomp.algebra.ssrint]
+_ - _ (int_scope) [notation, in mathcomp.algebra.ssrint]
+_ + _ (int_scope) [notation, in mathcomp.algebra.ssrint]
++%Z (int_scope) [notation, in mathcomp.algebra.ssrint]
+- _ (int_scope) [notation, in mathcomp.algebra.ssrint]
+-%Z (int_scope) [notation, in mathcomp.algebra.ssrint]
+0 (int_scope) [notation, in mathcomp.algebra.ssrint]
+intZmod.int_spec [inductive, in mathcomp.algebra.ssrint]
+intZmod.int_ind [definition, in mathcomp.algebra.ssrint]
+intZmod.int_rec [definition, in mathcomp.algebra.ssrint]
+intZmod.int_rect [lemma, in mathcomp.algebra.ssrint]
+intZmod.Mixin [definition, in mathcomp.algebra.ssrint]
+intZmod.NegzE [lemma, in mathcomp.algebra.ssrint]
+intZmod.oppz [definition, in mathcomp.algebra.ssrint]
+intZmod.oppzK [lemma, in mathcomp.algebra.ssrint]
+intZmod.oppz_add [lemma, in mathcomp.algebra.ssrint]
+intZmod.PoszD [lemma, in mathcomp.algebra.ssrint]
+intZmod.predn_int [lemma, in mathcomp.algebra.ssrint]
+intZmod.subSz1 [lemma, in mathcomp.algebra.ssrint]
+intZmod.ZintNeg [constructor, in mathcomp.algebra.ssrint]
+intZmod.ZintNull [constructor, in mathcomp.algebra.ssrint]
+intZmod.ZintPos [constructor, in mathcomp.algebra.ssrint]
+int_Smith_normal_form [lemma, in mathcomp.algebra.intdiv]
+int_spec [inductive, in mathcomp.algebra.ssrint]
+int_ind [definition, in mathcomp.algebra.ssrint]
+int_rec [definition, in mathcomp.algebra.ssrint]
+int_rect [lemma, in mathcomp.algebra.ssrint]
+int_choiceMixin [definition, in mathcomp.algebra.ssrint]
+int_countMixin [definition, in mathcomp.algebra.ssrint]
+int_eqMixin [definition, in mathcomp.algebra.ssrint]
+int_of_natsum [definition, in mathcomp.algebra.ssrint]
+invariant [definition, in mathcomp.ssreflect.eqtype]
+invariant_chief_irr_cases [lemma, in mathcomp.character.inertia]
+invariant_subnormal [lemma, in mathcomp.solvable.gseries]
+invariant_factor [definition, in mathcomp.solvable.gseries]
+invariant_inj [lemma, in mathcomp.ssreflect.eqtype]
+invariant_comp [lemma, in mathcomp.ssreflect.eqtype]
+invCg [lemma, in mathcomp.fingroup.fingroup]
+invDg [lemma, in mathcomp.fingroup.fingroup]
+InverseMorphism [section, in mathcomp.fingroup.morphism]
+InverseMorphism.aT [variable, in mathcomp.fingroup.morphism]
+InverseMorphism.f [variable, in mathcomp.fingroup.morphism]
+InverseMorphism.G [variable, in mathcomp.fingroup.morphism]
+InverseMorphism.injf [variable, in mathcomp.fingroup.morphism]
+InverseMorphism.rT [variable, in mathcomp.fingroup.morphism]
+invF [definition, in mathcomp.ssreflect.fintype]
+invF_f [lemma, in mathcomp.ssreflect.fintype]
+invg [definition, in mathcomp.fingroup.fingroup]
+invGid [lemma, in mathcomp.fingroup.fingroup]
+invgK [lemma, in mathcomp.fingroup.fingroup]
+invg_expg [lemma, in mathcomp.fingroup.fingroup]
+invg_rcoset [lemma, in mathcomp.fingroup.fingroup]
+invg_lcoset [lemma, in mathcomp.fingroup.fingroup]
+invg_lcosets [lemma, in mathcomp.fingroup.fingroup]
+invg_set1 [lemma, in mathcomp.fingroup.fingroup]
+invg_comm [lemma, in mathcomp.fingroup.fingroup]
+invg_inj [lemma, in mathcomp.fingroup.fingroup]
+invg1 [lemma, in mathcomp.fingroup.fingroup]
+invg2id [lemma, in mathcomp.fingroup.fingroup]
+invIg [lemma, in mathcomp.fingroup.fingroup]
+invm [definition, in mathcomp.fingroup.morphism]
+invmE [lemma, in mathcomp.fingroup.morphism]
+invMG [lemma, in mathcomp.fingroup.fingroup]
+invMg [lemma, in mathcomp.fingroup.fingroup]
+invmK [lemma, in mathcomp.fingroup.morphism]
+InvMorphism [section, in mathcomp.character.classfun]
+InvMorphism.aT [variable, in mathcomp.character.classfun]
+InvMorphism.f [variable, in mathcomp.character.classfun]
+InvMorphism.G [variable, in mathcomp.character.classfun]
+InvMorphism.isoGR [variable, in mathcomp.character.classfun]
+InvMorphism.R [variable, in mathcomp.character.classfun]
+InvMorphism.rT [variable, in mathcomp.character.classfun]
+invmx [definition, in mathcomp.algebra.matrix]
+invmxK [lemma, in mathcomp.algebra.matrix]
+invmxZ [lemma, in mathcomp.algebra.matrix]
+invmx_out [lemma, in mathcomp.algebra.matrix]
+invmx_scalar [lemma, in mathcomp.algebra.matrix]
+invmx1 [lemma, in mathcomp.algebra.matrix]
+invm_subker [lemma, in mathcomp.fingroup.morphism]
+involutions_gen_dihedral [lemma, in mathcomp.solvable.extremal]
+invq [definition, in mathcomp.algebra.rat]
+InvQuotientSpec [constructor, in mathcomp.fingroup.quotient]
+invq_frac [lemma, in mathcomp.algebra.rat]
+invq_subdef [definition, in mathcomp.algebra.rat]
+invq0 [lemma, in mathcomp.algebra.rat]
+invr_lin_char [lemma, in mathcomp.character.character]
+invr_expz [lemma, in mathcomp.algebra.ssrint]
+invSg [lemma, in mathcomp.fingroup.fingroup]
+invUg [lemma, in mathcomp.fingroup.fingroup]
+inv_is_ahom [lemma, in mathcomp.field.galois]
+inv_kHomf [lemma, in mathcomp.field.galois]
+inv_quotientN [lemma, in mathcomp.fingroup.quotient]
+inv_quotientS [lemma, in mathcomp.fingroup.quotient]
+inv_quotient_spec [inductive, in mathcomp.fingroup.quotient]
+inv_lfun_def [lemma, in mathcomp.algebra.vector]
+inv_lfun [definition, in mathcomp.algebra.vector]
+inv_dprod_Iirr0 [lemma, in mathcomp.character.character]
+inv_dprod_IirrK [lemma, in mathcomp.character.character]
+inv_dprod_Iirr [definition, in mathcomp.character.character]
+inv_eq [lemma, in mathcomp.ssreflect.eqtype]
+inv_subG [lemma, in mathcomp.fingroup.fingroup]
+inZp [definition, in mathcomp.algebra.zmodp]
+in_factmod_module [lemma, in mathcomp.character.mxrepresentation]
+in_submod_module [lemma, in mathcomp.character.mxrepresentation]
+in_factmodJ [lemma, in mathcomp.character.mxrepresentation]
+in_submodJ [lemma, in mathcomp.character.mxrepresentation]
+in_factmodsK [lemma, in mathcomp.character.mxrepresentation]
+in_factmod_addsK [lemma, in mathcomp.character.mxrepresentation]
+in_factmodK [lemma, in mathcomp.character.mxrepresentation]
+in_factmod_eq0 [lemma, in mathcomp.character.mxrepresentation]
+in_factmodE [lemma, in mathcomp.character.mxrepresentation]
+in_factmod [definition, in mathcomp.character.mxrepresentation]
+in_submod_eq0 [lemma, in mathcomp.character.mxrepresentation]
+in_submodK [lemma, in mathcomp.character.mxrepresentation]
+in_submodE [lemma, in mathcomp.character.mxrepresentation]
+in_submod [definition, in mathcomp.character.mxrepresentation]
+in_tupleE [lemma, in mathcomp.ssreflect.tuple]
+in_tuple [definition, in mathcomp.ssreflect.tuple]
+in_Crat_span [definition, in mathcomp.field.algnum]
+in_nil [lemma, in mathcomp.ssreflect.seq]
+in_cons [lemma, in mathcomp.ssreflect.seq]
+in_iinv_f [lemma, in mathcomp.ssreflect.fintype]
+in_group [definition, in mathcomp.fingroup.fingroup]
+in_cprodM [lemma, in mathcomp.solvable.center]
+in_cprod [definition, in mathcomp.solvable.center]
+in_setX [lemma, in mathcomp.ssreflect.finset]
+in_setD [lemma, in mathcomp.ssreflect.finset]
+in_setC [lemma, in mathcomp.ssreflect.finset]
+in_setI [lemma, in mathcomp.ssreflect.finset]
+in_setU [lemma, in mathcomp.ssreflect.finset]
+in_set2 [lemma, in mathcomp.ssreflect.finset]
+in_setD1 [lemma, in mathcomp.ssreflect.finset]
+in_setC1 [lemma, in mathcomp.ssreflect.finset]
+in_setU1 [lemma, in mathcomp.ssreflect.finset]
+in_set1 [lemma, in mathcomp.ssreflect.finset]
+in_set0 [lemma, in mathcomp.ssreflect.finset]
+in_setT [lemma, in mathcomp.ssreflect.finset]
+in_set [lemma, in mathcomp.ssreflect.finset]
+iota [definition, in mathcomp.ssreflect.seq]
+iotaPz [abbreviation, in mathcomp.field.fieldext]
+iota_ltn_sorted [lemma, in mathcomp.ssreflect.path]
+iota_sorted [lemma, in mathcomp.ssreflect.path]
+iota_tupleP [lemma, in mathcomp.ssreflect.tuple]
+iota_uniq [lemma, in mathcomp.ssreflect.seq]
+iota_addl [lemma, in mathcomp.ssreflect.seq]
+iota_add [lemma, in mathcomp.ssreflect.seq]
+irr [definition, in mathcomp.character.character]
+IrrClass [section, in mathcomp.character.character]
+IrrClassDef [section, in mathcomp.character.character]
+IrrClassDef.G [variable, in mathcomp.character.character]
+IrrClassDef.gT [variable, in mathcomp.character.character]
+IrrClassDef.offset [variable, in mathcomp.character.character]
+IrrClassDef.sG [variable, in mathcomp.character.character]
+IrrClass.aG [variable, in mathcomp.character.character]
+IrrClass.closG [variable, in mathcomp.character.character]
+IrrClass.C'G [variable, in mathcomp.character.character]
+IrrClass.G [variable, in mathcomp.character.character]
+IrrClass.gT [variable, in mathcomp.character.character]
+IrrClass.R_G [variable, in mathcomp.character.character]
+IrrClass.sG [variable, in mathcomp.character.character]
+'e_ _ [notation, in mathcomp.character.character]
+'n_ _ [notation, in mathcomp.character.character]
+'R_ _ [notation, in mathcomp.character.character]
+IrrConstt [section, in mathcomp.character.character]
+IrrConstt.G [variable, in mathcomp.character.character]
+IrrConstt.gT [variable, in mathcomp.character.character]
+IrrConstt.H [variable, in mathcomp.character.character]
+irrEchar [lemma, in mathcomp.character.character]
+irredp_FAdjoin [lemma, in mathcomp.field.fieldext]
+irrK [lemma, in mathcomp.character.character]
+irrP [lemma, in mathcomp.character.character]
+irrRepr [lemma, in mathcomp.character.character]
+irrType [definition, in mathcomp.character.mxrepresentation]
+irrWchar [lemma, in mathcomp.character.character]
+irrWnorm [lemma, in mathcomp.character.character]
+irr_gring_center [lemma, in mathcomp.character.integral_char]
+irr_constt_to_dirr [lemma, in mathcomp.character.vcharacter]
+irr_dirr [lemma, in mathcomp.character.vcharacter]
+irr_vchar [lemma, in mathcomp.character.vcharacter]
+irr_vchar_on [lemma, in mathcomp.character.vcharacter]
+irr_modeV [lemma, in mathcomp.character.mxrepresentation]
+irr_mode_neq0 [lemma, in mathcomp.character.mxrepresentation]
+irr_mode_unit [lemma, in mathcomp.character.mxrepresentation]
+irr_modeX [lemma, in mathcomp.character.mxrepresentation]
+irr_modeM [lemma, in mathcomp.character.mxrepresentation]
+irr_center_scalar [lemma, in mathcomp.character.mxrepresentation]
+irr_mode1 [lemma, in mathcomp.character.mxrepresentation]
+irr_mode [definition, in mathcomp.character.mxrepresentation]
+irr_degree_abelian [lemma, in mathcomp.character.mxrepresentation]
+irr_mx_mult [lemma, in mathcomp.character.mxrepresentation]
+irr_comp_id [lemma, in mathcomp.character.mxrepresentation]
+irr_repr'_op0 [lemma, in mathcomp.character.mxrepresentation]
+irr_reprK [lemma, in mathcomp.character.mxrepresentation]
+irr_comp_rsim [lemma, in mathcomp.character.mxrepresentation]
+irr_comp_envelop [lemma, in mathcomp.character.mxrepresentation]
+irr_comp'_op0 [lemma, in mathcomp.character.mxrepresentation]
+irr_comp [definition, in mathcomp.character.mxrepresentation]
+irr_mx_sum [lemma, in mathcomp.character.mxrepresentation]
+irr_reprE [lemma, in mathcomp.character.mxrepresentation]
+irr_repr [definition, in mathcomp.character.mxrepresentation]
+irr_degree_gt0 [lemma, in mathcomp.character.mxrepresentation]
+irr_degreeE [lemma, in mathcomp.character.mxrepresentation]
+irr_degree [definition, in mathcomp.character.mxrepresentation]
+irr_faithful_center [lemma, in mathcomp.character.character]
+irr_cfcenterE [lemma, in mathcomp.character.character]
+irr_prime_injP [lemma, in mathcomp.character.character]
+irr_aut_closed [lemma, in mathcomp.character.character]
+irr_consttE [lemma, in mathcomp.character.character]
+irr_constt [definition, in mathcomp.character.character]
+irr_orthonormal [lemma, in mathcomp.character.character]
+irr_classK [lemma, in mathcomp.character.character]
+irr_classP [lemma, in mathcomp.character.character]
+irr_class [definition, in mathcomp.character.character]
+irr_inv [lemma, in mathcomp.character.character]
+irr_prime_lin [lemma, in mathcomp.character.character]
+irr_cyclic_lin [lemma, in mathcomp.character.character]
+irr_repr_lin_char [lemma, in mathcomp.character.character]
+irr_char [lemma, in mathcomp.character.character]
+irr_reprP [lemma, in mathcomp.character.character]
+irr_basis [lemma, in mathcomp.character.character]
+irr_eq1 [lemma, in mathcomp.character.character]
+irr_inj [lemma, in mathcomp.character.character]
+irr_free [lemma, in mathcomp.character.character]
+irr_sum_square [lemma, in mathcomp.character.character]
+irr_neq0 [lemma, in mathcomp.character.character]
+irr_def [definition, in mathcomp.character.character]
+irr_key [lemma, in mathcomp.character.character]
+irr_of_socle_bij [lemma, in mathcomp.character.character]
+irr_of_socleK [lemma, in mathcomp.character.character]
+irr_of_socle [definition, in mathcomp.character.character]
+irr_induced_Frobenius_ker [lemma, in mathcomp.character.inertia]
+irr0 [lemma, in mathcomp.character.character]
+irr1_mode [lemma, in mathcomp.character.mxrepresentation]
+irr1_repr [lemma, in mathcomp.character.mxrepresentation]
+irr1_rfix [lemma, in mathcomp.character.mxrepresentation]
+irr1_abelian_bound [lemma, in mathcomp.character.character]
+irr1_bound [lemma, in mathcomp.character.character]
+irr1_neq0 [lemma, in mathcomp.character.character]
+irr1_gt0 [lemma, in mathcomp.character.character]
+irr1_degree [lemma, in mathcomp.character.character]
+IsChar [section, in mathcomp.character.character]
+IsChar.G [variable, in mathcomp.character.character]
+IsChar.gT [variable, in mathcomp.character.character]
+isgroupP [lemma, in mathcomp.fingroup.fingroup]
+IsMxvecIndex [constructor, in mathcomp.algebra.matrix]
+isnull [definition, in mathcomp.field.closed_field]
+isnullP [lemma, in mathcomp.field.closed_field]
+isnull_qf [lemma, in mathcomp.field.closed_field]
+isob [abbreviation, in mathcomp.solvable.center]
+IsoBoolEquiv [section, in mathcomp.fingroup.morphism]
+IsoBoolEquiv.G [variable, in mathcomp.fingroup.morphism]
+IsoBoolEquiv.gT [variable, in mathcomp.fingroup.morphism]
+IsoBoolEquiv.H [variable, in mathcomp.fingroup.morphism]
+IsoBoolEquiv.hT [variable, in mathcomp.fingroup.morphism]
+IsoBoolEquiv.K [variable, in mathcomp.fingroup.morphism]
+IsoBoolEquiv.kT [variable, in mathcomp.fingroup.morphism]
+IsoCyclic [section, in mathcomp.solvable.cyclic]
+IsoCyclic.gT [variable, in mathcomp.solvable.cyclic]
+IsoCyclic.rT [variable, in mathcomp.solvable.cyclic]
+IsoFitting [section, in mathcomp.solvable.maximal]
+IsoFitting.D [variable, in mathcomp.solvable.maximal]
+IsoFitting.f [variable, in mathcomp.solvable.maximal]
+IsoFitting.G [variable, in mathcomp.solvable.maximal]
+IsoFitting.gT [variable, in mathcomp.solvable.maximal]
+IsoFitting.rT [variable, in mathcomp.solvable.maximal]
+IsoFunctorTheory [section, in mathcomp.solvable.gfunctor]
+IsoFunctorTheory.F [variable, in mathcomp.solvable.gfunctor]
+Isog [section, in mathcomp.solvable.pgroup]
+isog [definition, in mathcomp.fingroup.morphism]
+IsogAbelem [section, in mathcomp.solvable.abelian]
+IsogAbelem.aT [variable, in mathcomp.solvable.abelian]
+IsogAbelem.G [variable, in mathcomp.solvable.abelian]
+IsogAbelem.H [variable, in mathcomp.solvable.abelian]
+IsogAbelem.isoGH [variable, in mathcomp.solvable.abelian]
+IsogAbelem.rT [variable, in mathcomp.solvable.abelian]
+IsogAbelian [section, in mathcomp.solvable.abelian]
+IsogAbelian.aT [variable, in mathcomp.solvable.abelian]
+IsogAbelian.D [variable, in mathcomp.solvable.abelian]
+IsogAbelian.f [variable, in mathcomp.solvable.abelian]
+IsogAbelian.rT [variable, in mathcomp.solvable.abelian]
+isogEcard [lemma, in mathcomp.fingroup.morphism]
+isogEhom [lemma, in mathcomp.fingroup.morphism]
+isogP [lemma, in mathcomp.fingroup.morphism]
+isoGrpP [lemma, in mathcomp.fingroup.presentation]
+isoGrp_trans [lemma, in mathcomp.fingroup.presentation]
+isoGrp_hom [lemma, in mathcomp.fingroup.presentation]
+isog_pseries [lemma, in mathcomp.solvable.pgroup]
+isog_pcore [lemma, in mathcomp.solvable.pgroup]
+isog_pgroup [lemma, in mathcomp.solvable.pgroup]
+isog_dprod [lemma, in mathcomp.fingroup.gproduct]
+isog_set1X [lemma, in mathcomp.fingroup.gproduct]
+isog_setX1 [lemma, in mathcomp.fingroup.gproduct]
+isog_2extraspecial [lemma, in mathcomp.solvable.extraspecial]
+isog_2X1p2 [lemma, in mathcomp.solvable.extraspecial]
+isog_pX1p2n [lemma, in mathcomp.solvable.extraspecial]
+isog_pX1p2 [lemma, in mathcomp.solvable.extraspecial]
+isog_homocyclic [lemma, in mathcomp.solvable.abelian]
+isog_abelem_card [lemma, in mathcomp.solvable.abelian]
+isog_abelian_type [lemma, in mathcomp.solvable.abelian]
+isog_Mho [lemma, in mathcomp.solvable.abelian]
+isog_Ohm [lemma, in mathcomp.solvable.abelian]
+isog_rank [lemma, in mathcomp.solvable.abelian]
+isog_p_rank [lemma, in mathcomp.solvable.abelian]
+isog_grank [lemma, in mathcomp.solvable.abelian]
+isog_abelem [lemma, in mathcomp.solvable.abelian]
+isog_simple [lemma, in mathcomp.solvable.gseries]
+isog_extraspecial [lemma, in mathcomp.solvable.maximal]
+isog_special [lemma, in mathcomp.solvable.maximal]
+isog_Fitting [lemma, in mathcomp.solvable.maximal]
+isog_Phi [lemma, in mathcomp.solvable.maximal]
+isog_abelem_rV [lemma, in mathcomp.character.mxabelem]
+isog_sol [lemma, in mathcomp.solvable.nilpotent]
+isog_nil_class [lemma, in mathcomp.solvable.nilpotent]
+isog_nil [lemma, in mathcomp.solvable.nilpotent]
+isog_der [lemma, in mathcomp.solvable.commutator]
+isog_subg [lemma, in mathcomp.fingroup.morphism]
+isog_hom [lemma, in mathcomp.fingroup.morphism]
+isog_transr [lemma, in mathcomp.fingroup.morphism]
+isog_transl [lemma, in mathcomp.fingroup.morphism]
+isog_sym [lemma, in mathcomp.fingroup.morphism]
+isog_trans [lemma, in mathcomp.fingroup.morphism]
+isog_symr [lemma, in mathcomp.fingroup.morphism]
+isog_eq1 [lemma, in mathcomp.fingroup.morphism]
+isog_abelian [lemma, in mathcomp.fingroup.morphism]
+isog_refl [lemma, in mathcomp.fingroup.morphism]
+isog_isom [lemma, in mathcomp.fingroup.morphism]
+isog_xcprod [lemma, in mathcomp.solvable.center]
+isog_cprod_by [lemma, in mathcomp.solvable.center]
+isog_center [lemma, in mathcomp.solvable.center]
+isog_cyclic_card [lemma, in mathcomp.solvable.cyclic]
+isog_cyclic [lemma, in mathcomp.solvable.cyclic]
+Isog.aT [variable, in mathcomp.solvable.pgroup]
+Isog.G [variable, in mathcomp.solvable.pgroup]
+Isog.H [variable, in mathcomp.solvable.pgroup]
+Isog.rT [variable, in mathcomp.solvable.pgroup]
+Isom [section, in mathcomp.character.character]
+isom [definition, in mathcomp.fingroup.morphism]
+Isometries [section, in mathcomp.character.vcharacter]
+isometries [definition, in mathcomp.solvable.burnside_app]
+isometries_iso [lemma, in mathcomp.solvable.burnside_app]
+Isometries.G [variable, in mathcomp.character.vcharacter]
+Isometries.gT [variable, in mathcomp.character.vcharacter]
+Isometries.L [variable, in mathcomp.character.vcharacter]
+Isometries.S [variable, in mathcomp.character.vcharacter]
+isometries2 [definition, in mathcomp.solvable.burnside_app]
+isometry [definition, in mathcomp.character.classfun]
+isometry_in_zchar [lemma, in mathcomp.character.vcharacter]
+isometry_raddf_inj [lemma, in mathcomp.character.classfun]
+isometry_of_cfnorm [lemma, in mathcomp.character.classfun]
+isometry_of_free [lemma, in mathcomp.character.classfun]
+isometry_from_to [definition, in mathcomp.character.classfun]
+IsomInv [section, in mathcomp.character.character]
+IsomInv.aT [variable, in mathcomp.character.character]
+IsomInv.f [variable, in mathcomp.character.character]
+IsomInv.G [variable, in mathcomp.character.character]
+IsomInv.isoGR [variable, in mathcomp.character.character]
+IsomInv.R [variable, in mathcomp.character.character]
+IsomInv.rT [variable, in mathcomp.character.character]
+Isomorphism [section, in mathcomp.character.classfun]
+Isomorphisms [section, in mathcomp.fingroup.morphism]
+Isomorphisms.G [variable, in mathcomp.fingroup.morphism]
+Isomorphisms.gT [variable, in mathcomp.fingroup.morphism]
+Isomorphisms.H [variable, in mathcomp.fingroup.morphism]
+Isomorphisms.hT [variable, in mathcomp.fingroup.morphism]
+Isomorphisms.K [variable, in mathcomp.fingroup.morphism]
+Isomorphisms.kT [variable, in mathcomp.fingroup.morphism]
+Isomorphism.aT [variable, in mathcomp.character.classfun]
+Isomorphism.defG [variable, in mathcomp.character.classfun]
+Isomorphism.defR [variable, in mathcomp.character.classfun]
+Isomorphism.f [variable, in mathcomp.character.classfun]
+Isomorphism.G [variable, in mathcomp.character.classfun]
+Isomorphism.isoGR [variable, in mathcomp.character.classfun]
+Isomorphism.R [variable, in mathcomp.character.classfun]
+Isomorphism.rT [variable, in mathcomp.character.classfun]
+isomP [lemma, in mathcomp.fingroup.morphism]
+isom_IirrKV [lemma, in mathcomp.character.character]
+isom_IirrK [lemma, in mathcomp.character.character]
+isom_Iirr0 [lemma, in mathcomp.character.character]
+isom_Iirr_eq0 [lemma, in mathcomp.character.character]
+isom_Iirr_inj [lemma, in mathcomp.character.character]
+isom_IirrE [lemma, in mathcomp.character.character]
+isom_Iirr [definition, in mathcomp.character.character]
+isom_restr_perm [lemma, in mathcomp.fingroup.action]
+isom_sgval [lemma, in mathcomp.fingroup.morphism]
+isom_subg [lemma, in mathcomp.fingroup.morphism]
+isom_sym [lemma, in mathcomp.fingroup.morphism]
+isom_inv [definition, in mathcomp.fingroup.morphism]
+isom_sub_im [lemma, in mathcomp.fingroup.morphism]
+isom_card [lemma, in mathcomp.fingroup.morphism]
+isom_im [lemma, in mathcomp.fingroup.morphism]
+isom_inj [lemma, in mathcomp.fingroup.morphism]
+isom_isog [lemma, in mathcomp.fingroup.morphism]
+Isom.aT [variable, in mathcomp.character.character]
+Isom.f [variable, in mathcomp.character.character]
+Isom.G [variable, in mathcomp.character.character]
+Isom.isoGR [variable, in mathcomp.character.character]
+Isom.R [variable, in mathcomp.character.character]
+Isom.rT [variable, in mathcomp.character.character]
+iso_eq_F0_F1_F2 [lemma, in mathcomp.solvable.burnside_app]
+iso_eq_F0_F1 [lemma, in mathcomp.solvable.burnside_app]
+iso0_1 [lemma, in mathcomp.solvable.burnside_app]
+iso3 [definition, in mathcomp.solvable.burnside_app]
+iso3l [definition, in mathcomp.solvable.burnside_app]
+iso3_ndir [lemma, in mathcomp.solvable.burnside_app]
+isSome_insub [lemma, in mathcomp.ssreflect.eqtype]
+is_perm_mxV [lemma, in mathcomp.algebra.matrix]
+is_perm_mxMr [lemma, in mathcomp.algebra.matrix]
+is_perm_mx_tr [lemma, in mathcomp.algebra.matrix]
+is_perm_mxMl [lemma, in mathcomp.algebra.matrix]
+is_perm_mx1 [lemma, in mathcomp.algebra.matrix]
+is_perm_mxP [lemma, in mathcomp.algebra.matrix]
+is_perm_mx [definition, in mathcomp.algebra.matrix]
+is_scalar_mxP [lemma, in mathcomp.algebra.matrix]
+is_scalar_mx [definition, in mathcomp.algebra.matrix]
+is_mxvec_index [inductive, in mathcomp.algebra.matrix]
+is_abelemP [lemma, in mathcomp.solvable.abelian]
+is_abelem_pgroup [lemma, in mathcomp.solvable.abelian]
+is_abelem [definition, in mathcomp.solvable.abelian]
+is_groupAction [definition, in mathcomp.fingroup.action]
+is_total_action [lemma, in mathcomp.fingroup.action]
+is_action [definition, in mathcomp.fingroup.action]
+is_class_fun [definition, in mathcomp.character.classfun]
+is_aspace [definition, in mathcomp.field.falgebra]
+is_algid [definition, in mathcomp.field.falgebra]
+is_iso3P [lemma, in mathcomp.solvable.burnside_app]
+is_iso3b [definition, in mathcomp.solvable.burnside_app]
+is_iso3 [definition, in mathcomp.solvable.burnside_app]
+is_isoP [lemma, in mathcomp.solvable.burnside_app]
+is_iso [definition, in mathcomp.solvable.burnside_app]
+is_rot [definition, in mathcomp.solvable.burnside_app]
+is_transversal [definition, in mathcomp.ssreflect.finset]
+iter [definition, in mathcomp.ssreflect.ssrnat]
+Iteration [section, in mathcomp.ssreflect.ssrnat]
+Iteration.T [variable, in mathcomp.ssreflect.ssrnat]
+IterCprod [section, in mathcomp.solvable.center]
+IterCprod.G [variable, in mathcomp.solvable.center]
+IterCprod.gT [variable, in mathcomp.solvable.center]
+iteri [definition, in mathcomp.ssreflect.ssrnat]
+iteriS [lemma, in mathcomp.ssreflect.ssrnat]
+iterop [definition, in mathcomp.ssreflect.ssrnat]
+iteropS [lemma, in mathcomp.ssreflect.ssrnat]
+iterS [lemma, in mathcomp.ssreflect.ssrnat]
+iterSr [lemma, in mathcomp.ssreflect.ssrnat]
+iter_pcycle [lemma, in mathcomp.fingroup.perm]
+iter_muln_1 [lemma, in mathcomp.ssreflect.ssrnat]
+iter_muln [lemma, in mathcomp.ssreflect.ssrnat]
+iter_addn_0 [lemma, in mathcomp.ssreflect.ssrnat]
+iter_addn [lemma, in mathcomp.ssreflect.ssrnat]
+iter_predn [lemma, in mathcomp.ssreflect.ssrnat]
+iter_succn_0 [lemma, in mathcomp.ssreflect.ssrnat]
+iter_succn [lemma, in mathcomp.ssreflect.ssrnat]
+iter_add [lemma, in mathcomp.ssreflect.ssrnat]
+iter_finv [lemma, in mathcomp.ssreflect.fingraph]
+iter_order [lemma, in mathcomp.ssreflect.fingraph]
+iter_finv_in [lemma, in mathcomp.ssreflect.fingraph]
+iter_order_in [lemma, in mathcomp.ssreflect.fingraph]
+iter_in [lemma, in mathcomp.ssreflect.fingraph]
+iter_findex [lemma, in mathcomp.ssreflect.fingraph]
+itvP [lemma, in mathcomp.algebra.interval]
+itv_splitU2 [lemma, in mathcomp.algebra.interval]
+itv_splitU [lemma, in mathcomp.algebra.interval]
+itv_splitI [lemma, in mathcomp.algebra.interval]
+itv_gte [lemma, in mathcomp.algebra.interval]
+itv_xx [lemma, in mathcomp.algebra.interval]
+itv_boundlr [lemma, in mathcomp.algebra.interval]
+itv_dec [lemma, in mathcomp.algebra.interval]
+itv_decompose [definition, in mathcomp.algebra.interval]
+itv_rewrite [definition, in mathcomp.algebra.interval]
+itv_bound [inductive, in mathcomp.algebra.interval]
+
| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +