| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 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]
-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]
-incrn_inj_in [lemma, in mathcomp.ssreflect.ssrnat]
-incrn_inj [lemma, in mathcomp.ssreflect.ssrnat]
-incr_tallyP [lemma, in mathcomp.ssreflect.seq]
-incr_tally [definition, in mathcomp.ssreflect.seq]
-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.ssrbool]
-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]
-InheritedStructures [section, in mathcomp.ssreflect.finfun]
-InheritedStructures.aT [variable, in mathcomp.ssreflect.finfun]
-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_homo [lemma, in mathcomp.ssreflect.eqtype]
-inj_homo_in [lemma, in mathcomp.ssreflect.eqtype]
-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]
-IntervalEq [section, in mathcomp.algebra.interval]
-IntervalEq.T [variable, in mathcomp.algebra.interval]
-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]
-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]
-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_intersectionA [lemma, in mathcomp.algebra.interval]
-itv_intersectionC [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_intersectionii [lemma, in mathcomp.algebra.interval]
-itv_intersectioni1 [definition, in mathcomp.algebra.interval]
-itv_intersection1i [definition, in mathcomp.algebra.interval]
-itv_intersection [definition, 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -