| 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 (lemma)
+idealMr [in mathcomp.algebra.ring_quotient]+idealr_closedB [in mathcomp.algebra.ring_quotient]
+idealr_closed_nontrivial [in mathcomp.algebra.ring_quotient]
+idealr0 [in mathcomp.algebra.ring_quotient]
+idealr1 [in mathcomp.algebra.ring_quotient]
+idGfun_monotonic [in mathcomp.solvable.gfunctor]
+idGfun_cont [in mathcomp.solvable.gfunctor]
+idGfun_closed [in mathcomp.solvable.gfunctor]
+idmxE [in mathcomp.algebra.matrix]
+idm_isom [in mathcomp.fingroup.morphism]
+idm_morphM [in mathcomp.fingroup.morphism]
+id_lfunE [in mathcomp.algebra.vector]
+id_is_ahom [in mathcomp.field.falgebra]
+ieexprIz [in mathcomp.algebra.ssrint]
+ifactmE [in mathcomp.fingroup.morphism]
+ifnzP [in mathcomp.ssreflect.prime]
+ifN_eqC [in mathcomp.ssreflect.eqtype]
+ifN_eq [in mathcomp.ssreflect.eqtype]
+iinv_f [in mathcomp.ssreflect.fintype]
+iinv_proof [in mathcomp.ssreflect.fintype]
+Iirr_cast [in mathcomp.character.character]
+Iirr1_neq0 [in mathcomp.character.character]
+imageP [in mathcomp.ssreflect.fintype]
+image_injP [in mathcomp.ssreflect.fintype]
+image_pre [in mathcomp.ssreflect.fintype]
+image_iinv [in mathcomp.ssreflect.fintype]
+image_pred0 [in mathcomp.ssreflect.fintype]
+image_codom [in mathcomp.ssreflect.fintype]
+image_f [in mathcomp.ssreflect.fintype]
+imsetI [in mathcomp.ssreflect.finset]
+imsetP [in mathcomp.ssreflect.finset]
+imsetS [in mathcomp.ssreflect.finset]
+imsetU [in mathcomp.ssreflect.finset]
+imsetU1 [in mathcomp.ssreflect.finset]
+imset_coset [in mathcomp.fingroup.quotient]
+imset_mulgm [in mathcomp.fingroup.gproduct]
+imset_autE [in mathcomp.fingroup.automorphism]
+imset_comp [in mathcomp.ssreflect.finset]
+imset_id [in mathcomp.ssreflect.finset]
+imset_injP [in mathcomp.ssreflect.finset]
+imset_card [in mathcomp.ssreflect.finset]
+imset_proper [in mathcomp.ssreflect.finset]
+imset_set1 [in mathcomp.ssreflect.finset]
+imset_eq0 [in mathcomp.ssreflect.finset]
+Imset.imsetE [in mathcomp.ssreflect.finset]
+Imset.imset2E [in mathcomp.ssreflect.finset]
+imset0 [in mathcomp.ssreflect.finset]
+imset2P [in mathcomp.ssreflect.finset]
+imset2S [in mathcomp.ssreflect.finset]
+imset2Sl [in mathcomp.ssreflect.finset]
+imset2Sr [in mathcomp.ssreflect.finset]
+imset2Ul [in mathcomp.ssreflect.finset]
+imset2Ur [in mathcomp.ssreflect.finset]
+imset2_set1r [in mathcomp.ssreflect.finset]
+imset2_set1l [in mathcomp.ssreflect.finset]
+imset2_pair [in mathcomp.ssreflect.finset]
+im_qisom [in mathcomp.fingroup.quotient]
+im_qisom_proof [in mathcomp.fingroup.quotient]
+im_quotient [in mathcomp.fingroup.quotient]
+im_coset [in mathcomp.fingroup.quotient]
+im_perm_on [in mathcomp.fingroup.perm]
+im_permV [in mathcomp.fingroup.perm]
+im_xsdprodm [in mathcomp.fingroup.gproduct]
+im_sdprodm2 [in mathcomp.fingroup.gproduct]
+im_sdprodm1 [in mathcomp.fingroup.gproduct]
+im_dprodm [in mathcomp.fingroup.gproduct]
+im_cprodm [in mathcomp.fingroup.gproduct]
+im_sdprodm [in mathcomp.fingroup.gproduct]
+im_sdpair [in mathcomp.fingroup.gproduct]
+im_sdpair_TI [in mathcomp.fingroup.gproduct]
+im_sdpair_norm [in mathcomp.fingroup.gproduct]
+im_Aut_isom [in mathcomp.fingroup.automorphism]
+im_autm [in mathcomp.fingroup.automorphism]
+im_cfclass_Iirr [in mathcomp.character.inertia]
+im_actm [in mathcomp.fingroup.action]
+im_actperm_Aut [in mathcomp.fingroup.action]
+im_restr_perm [in mathcomp.fingroup.action]
+im_rVabelem [in mathcomp.character.mxabelem]
+im_abelem_rV [in mathcomp.character.mxabelem]
+im_sgval [in mathcomp.fingroup.morphism]
+im_subg [in mathcomp.fingroup.morphism]
+im_ifactm [in mathcomp.fingroup.morphism]
+im_invm [in mathcomp.fingroup.morphism]
+im_restrm [in mathcomp.fingroup.morphism]
+im_idm [in mathcomp.fingroup.morphism]
+im_xcprodmr [in mathcomp.solvable.center]
+im_xcprodml [in mathcomp.solvable.center]
+im_xcprodm [in mathcomp.solvable.center]
+im_cpair_cprod [in mathcomp.solvable.center]
+im_cpair [in mathcomp.solvable.center]
+im_cpair_cent [in mathcomp.solvable.center]
+im_Zp_unitm [in mathcomp.solvable.cyclic]
+im_cyclem [in mathcomp.solvable.cyclic]
+im_eltm [in mathcomp.solvable.cyclic]
+im_Zpm [in mathcomp.solvable.cyclic]
+im_transversal_repr [in mathcomp.ssreflect.finset]
+incr_nthC [in mathcomp.ssreflect.seq]
+incr_nth_inj [in mathcomp.ssreflect.seq]
+indexgg [in mathcomp.fingroup.fingroup]
+indexgI [in mathcomp.fingroup.fingroup]
+indexgS [in mathcomp.fingroup.fingroup]
+indexg_gt1 [in mathcomp.fingroup.fingroup]
+indexg_eq1 [in mathcomp.fingroup.fingroup]
+indexg_gt0 [in mathcomp.fingroup.fingroup]
+indexg1 [in mathcomp.fingroup.fingroup]
+indexJg [in mathcomp.fingroup.fingroup]
+indexMg [in mathcomp.fingroup.fingroup]
+indexSg [in mathcomp.fingroup.fingroup]
+index_support_dvd_degree [in mathcomp.character.integral_char]
+index_cosetpre [in mathcomp.fingroup.quotient]
+index_quotient_eq [in mathcomp.fingroup.quotient]
+index_quotient [in mathcomp.fingroup.quotient]
+index_quotient_ker [in mathcomp.fingroup.quotient]
+index_morphpre [in mathcomp.fingroup.quotient]
+index_injm [in mathcomp.fingroup.quotient]
+index_morphim [in mathcomp.fingroup.quotient]
+index_morphim_ker [in mathcomp.fingroup.quotient]
+index_sdprodr [in mathcomp.fingroup.gproduct]
+index_sdprod [in mathcomp.fingroup.gproduct]
+index_map [in mathcomp.ssreflect.seq]
+index_last [in mathcomp.ssreflect.seq]
+index_head [in mathcomp.ssreflect.seq]
+index_uniq [in mathcomp.ssreflect.seq]
+index_cat [in mathcomp.ssreflect.seq]
+index_mem [in mathcomp.ssreflect.seq]
+index_size [in mathcomp.ssreflect.seq]
+index_maxnormal_sol_prime [in mathcomp.solvable.maximal]
+index_enum_ord [in mathcomp.ssreflect.fintype]
+index_cent1 [in mathcomp.fingroup.action]
+index1g [in mathcomp.fingroup.fingroup]
+index2_normal [in mathcomp.fingroup.fingroup]
+Ind_irr_neq0 [in mathcomp.character.character]
+inertiaJ [in mathcomp.character.inertia]
+inertia_Frobenius_ker [in mathcomp.character.inertia]
+inertia_bigdprod_irr [in mathcomp.character.inertia]
+inertia_bigdprod [in mathcomp.character.inertia]
+inertia_bigdprodi [in mathcomp.character.inertia]
+inertia_dprod_irr [in mathcomp.character.inertia]
+inertia_dprod [in mathcomp.character.inertia]
+inertia_dprodr [in mathcomp.character.inertia]
+inertia_dprodl [in mathcomp.character.inertia]
+inertia_sdprod [in mathcomp.character.inertia]
+inertia_quo [in mathcomp.character.inertia]
+inertia_mod_quo [in mathcomp.character.inertia]
+inertia_mod_pre [in mathcomp.character.inertia]
+inertia_isom [in mathcomp.character.inertia]
+inertia_morph_im [in mathcomp.character.inertia]
+inertia_morph_pre [in mathcomp.character.inertia]
+inertia_id [in mathcomp.character.inertia]
+inertia_irr0 [in mathcomp.character.inertia]
+inertia_irr_prime [in mathcomp.character.inertia]
+inertia_injective [in mathcomp.character.inertia]
+inertia_prod [in mathcomp.character.inertia]
+inertia_mul [in mathcomp.character.inertia]
+inertia_opp [in mathcomp.character.inertia]
+inertia_scale_nz [in mathcomp.character.inertia]
+inertia_scale [in mathcomp.character.inertia]
+inertia_sum [in mathcomp.character.inertia]
+inertia_add [in mathcomp.character.inertia]
+Inertia_sub [in mathcomp.character.inertia]
+inertia_valJ [in mathcomp.character.inertia]
+inertia0 [in mathcomp.character.inertia]
+Inertia1 [in mathcomp.character.inertia]
+inertia1 [in mathcomp.character.inertia]
+injectiveP [in mathcomp.ssreflect.fintype]
+injectivePn [in mathcomp.ssreflect.fintype]
+injF_bij [in mathcomp.ssreflect.fintype]
+injF_onto [in mathcomp.ssreflect.fintype]
+injmD1 [in mathcomp.fingroup.morphism]
+injmF [in mathcomp.solvable.gfunctor]
+injmF_sub [in mathcomp.solvable.gfunctor]
+injmI [in mathcomp.fingroup.morphism]
+injmK [in mathcomp.fingroup.morphism]
+injmP [in mathcomp.fingroup.morphism]
+injmSK [in mathcomp.fingroup.morphism]
+injm_pseries [in mathcomp.solvable.pgroup]
+injm_pcore [in mathcomp.solvable.pgroup]
+injm_pHall [in mathcomp.solvable.pgroup]
+injm_pelt [in mathcomp.solvable.pgroup]
+injm_pgroup [in mathcomp.solvable.pgroup]
+injm_qisom [in mathcomp.fingroup.quotient]
+injm_quotm [in mathcomp.fingroup.quotient]
+injm_Frobenius_group [in mathcomp.solvable.frobenius]
+injm_Frobenius_ker [in mathcomp.solvable.frobenius]
+injm_Frobenius [in mathcomp.solvable.frobenius]
+injm_Frobenius_compl [in mathcomp.solvable.frobenius]
+injm_xsdprodm [in mathcomp.fingroup.gproduct]
+injm_dprodm [in mathcomp.fingroup.gproduct]
+injm_cprodm [in mathcomp.fingroup.gproduct]
+injm_sdprodm [in mathcomp.fingroup.gproduct]
+injm_pprodm [in mathcomp.fingroup.gproduct]
+injm_sdpair2 [in mathcomp.fingroup.gproduct]
+injm_sdpair1 [in mathcomp.fingroup.gproduct]
+injm_pairg1 [in mathcomp.fingroup.gproduct]
+injm_pair1g [in mathcomp.fingroup.gproduct]
+injm_bigdprod [in mathcomp.fingroup.gproduct]
+injm_dprod [in mathcomp.fingroup.gproduct]
+injm_sdprod [in mathcomp.fingroup.gproduct]
+injm_char [in mathcomp.fingroup.automorphism]
+injm_conj [in mathcomp.fingroup.automorphism]
+injm_Aut [in mathcomp.fingroup.automorphism]
+injm_Aut_isom [in mathcomp.fingroup.automorphism]
+injm_autm [in mathcomp.fingroup.automorphism]
+injm_Ohm [in mathcomp.solvable.abelian]
+injm_rank [in mathcomp.solvable.abelian]
+injm_p_rank [in mathcomp.solvable.abelian]
+injm_grank [in mathcomp.solvable.abelian]
+injm_pmaxElem [in mathcomp.solvable.abelian]
+injm_nElem [in mathcomp.solvable.abelian]
+injm_pnElem [in mathcomp.solvable.abelian]
+injm_pElem [in mathcomp.solvable.abelian]
+injm_abelem [in mathcomp.solvable.abelian]
+injm_Ldiv [in mathcomp.solvable.abelian]
+injm_minnormal [in mathcomp.solvable.gseries]
+injm_maxnormal [in mathcomp.solvable.gseries]
+injm_maximal_eq [in mathcomp.solvable.gseries]
+injm_maximal [in mathcomp.solvable.gseries]
+injm_extraspecial [in mathcomp.solvable.maximal]
+injm_special [in mathcomp.solvable.maximal]
+injm_Fitting [in mathcomp.solvable.maximal]
+injm_Phi [in mathcomp.solvable.maximal]
+injm_actm [in mathcomp.fingroup.action]
+injm_Aut_full [in mathcomp.fingroup.action]
+injm_Aut_sub [in mathcomp.fingroup.action]
+injm_faithful [in mathcomp.fingroup.action]
+injm_sol [in mathcomp.solvable.nilpotent]
+injm_nil [in mathcomp.solvable.nilpotent]
+injm_ucn [in mathcomp.solvable.nilpotent]
+injm_subg [in mathcomp.fingroup.morphism]
+injm_sgval [in mathcomp.fingroup.morphism]
+injm_ifactm [in mathcomp.fingroup.morphism]
+injm_invm [in mathcomp.fingroup.morphism]
+injm_proper [in mathcomp.fingroup.morphism]
+injm_factmP [in mathcomp.fingroup.morphism]
+injm_factm [in mathcomp.fingroup.morphism]
+injm_comp [in mathcomp.fingroup.morphism]
+injm_restrm [in mathcomp.fingroup.morphism]
+injm_idm [in mathcomp.fingroup.morphism]
+injm_abelian [in mathcomp.fingroup.morphism]
+injm_subcent [in mathcomp.fingroup.morphism]
+injm_cents [in mathcomp.fingroup.morphism]
+injm_cent [in mathcomp.fingroup.morphism]
+injm_subcent1 [in mathcomp.fingroup.morphism]
+injm_cent1 [in mathcomp.fingroup.morphism]
+injm_subnorm [in mathcomp.fingroup.morphism]
+injm_normal [in mathcomp.fingroup.morphism]
+injm_norms [in mathcomp.fingroup.morphism]
+injm_norm [in mathcomp.fingroup.morphism]
+injm_eq [in mathcomp.fingroup.morphism]
+injm_morphim_inj [in mathcomp.fingroup.morphism]
+injm_xcprodm [in mathcomp.solvable.center]
+injm_cpair1g [in mathcomp.solvable.center]
+injm_cpairg1 [in mathcomp.solvable.center]
+injm_center [in mathcomp.solvable.center]
+injm_Zp_unitm [in mathcomp.solvable.cyclic]
+injm_cyclem [in mathcomp.solvable.cyclic]
+injm_generator [in mathcomp.solvable.cyclic]
+injm_cyclic [in mathcomp.solvable.cyclic]
+injm_eltm [in mathcomp.solvable.cyclic]
+injm_Zpm [in mathcomp.solvable.cyclic]
+injm1 [in mathcomp.fingroup.morphism]
+inj_tperm [in mathcomp.fingroup.perm]
+inj_map [in mathcomp.ssreflect.seq]
+inj_card_bij [in mathcomp.ssreflect.fintype]
+inj_card_onto [in mathcomp.ssreflect.fintype]
+inj_eqAxiom [in mathcomp.ssreflect.eqtype]
+inj_in_eq [in mathcomp.ssreflect.eqtype]
+inj_eq [in mathcomp.ssreflect.eqtype]
+innew_val [in mathcomp.ssreflect.eqtype]
+inordK [in mathcomp.ssreflect.fintype]
+inord_val [in mathcomp.ssreflect.fintype]
+inseparable_sum [in mathcomp.field.separable]
+inseparable_add [in mathcomp.field.separable]
+insubdK [in mathcomp.ssreflect.eqtype]
+insubF [in mathcomp.ssreflect.eqtype]
+insubK [in mathcomp.ssreflect.eqtype]
+insubN [in mathcomp.ssreflect.eqtype]
+insubP [in mathcomp.ssreflect.eqtype]
+insubT [in mathcomp.ssreflect.eqtype]
+insub_eqE [in mathcomp.ssreflect.eqtype]
+intCK [in mathcomp.field.algC]
+IntDist.distnC [in mathcomp.algebra.ssrint]
+IntDist.distnDl [in mathcomp.algebra.ssrint]
+IntDist.distnDr [in mathcomp.algebra.ssrint]
+IntDist.distnEl [in mathcomp.algebra.ssrint]
+IntDist.distnEr [in mathcomp.algebra.ssrint]
+IntDist.distnn [in mathcomp.algebra.ssrint]
+IntDist.distnS [in mathcomp.algebra.ssrint]
+IntDist.distn_eq1 [in mathcomp.algebra.ssrint]
+IntDist.distn_eq0 [in mathcomp.algebra.ssrint]
+IntDist.distn0 [in mathcomp.algebra.ssrint]
+IntDist.distSn [in mathcomp.algebra.ssrint]
+IntDist.dist0n [in mathcomp.algebra.ssrint]
+IntDist.leqif_add_dist [in mathcomp.algebra.ssrint]
+IntDist.leqif_add_distz [in mathcomp.algebra.ssrint]
+IntDist.leq_add_dist [in mathcomp.algebra.ssrint]
+IntDist.sqrn_dist [in mathcomp.algebra.ssrint]
+integral_root [in mathcomp.algebra.mxpoly]
+integral_div [in mathcomp.algebra.mxpoly]
+integral_inv [in mathcomp.algebra.mxpoly]
+integral_algebraic [in mathcomp.algebra.mxpoly]
+integral_mul [in mathcomp.algebra.mxpoly]
+integral_add [in mathcomp.algebra.mxpoly]
+integral_sub [in mathcomp.algebra.mxpoly]
+integral_horner [in mathcomp.algebra.mxpoly]
+integral_opp [in mathcomp.algebra.mxpoly]
+integral_root_monic [in mathcomp.algebra.mxpoly]
+integral_horner_root [in mathcomp.algebra.mxpoly]
+integral_poly [in mathcomp.algebra.mxpoly]
+integral_nat [in mathcomp.algebra.mxpoly]
+integral_id [in mathcomp.algebra.mxpoly]
+integral_rmorph [in mathcomp.algebra.mxpoly]
+integral0 [in mathcomp.algebra.mxpoly]
+integral1 [in mathcomp.algebra.mxpoly]
+intEsg [in mathcomp.algebra.ssrint]
+intEsign [in mathcomp.algebra.ssrint]
+intmul1_is_rmorphism [in mathcomp.algebra.ssrint]
+intOrdered.abszN [in mathcomp.algebra.ssrint]
+intOrdered.eq0_normz [in mathcomp.algebra.ssrint]
+intOrdered.lez_def [in mathcomp.algebra.ssrint]
+intOrdered.lez_total [in mathcomp.algebra.ssrint]
+intOrdered.lez_norm_add [in mathcomp.algebra.ssrint]
+intOrdered.ltz_def [in mathcomp.algebra.ssrint]
+intOrdered.ltz_add [in mathcomp.algebra.ssrint]
+intOrdered.normzM [in mathcomp.algebra.ssrint]
+intOrdered.subz_ge0 [in mathcomp.algebra.ssrint]
+intP [in mathcomp.algebra.ssrint]
+intq_eq0 [in mathcomp.algebra.rat]
+intrD [in mathcomp.algebra.ssrint]
+intRing.mulNz [in mathcomp.algebra.ssrint]
+intRing.mulzA [in mathcomp.algebra.ssrint]
+intRing.mulzC [in mathcomp.algebra.ssrint]
+intRing.mulzN [in mathcomp.algebra.ssrint]
+intRing.mulzS [in mathcomp.algebra.ssrint]
+intRing.mulz_addl [in mathcomp.algebra.ssrint]
+intRing.mulz0 [in mathcomp.algebra.ssrint]
+intRing.mul0z [in mathcomp.algebra.ssrint]
+intRing.mul1z [in mathcomp.algebra.ssrint]
+intRing.nonzero1z [in mathcomp.algebra.ssrint]
+intrM [in mathcomp.algebra.ssrint]
+intro_mxsemisimple [in mathcomp.character.mxrepresentation]
+intro_unitmx [in mathcomp.algebra.matrix]
+intro_isoGrp [in mathcomp.fingroup.presentation]
+intro_class_fun [in mathcomp.character.classfun]
+intro_adjunction [in mathcomp.ssreflect.fingraph]
+intro_closed [in mathcomp.ssreflect.fingraph]
+intrV [in mathcomp.algebra.ssrint]
+intr_norm [in mathcomp.algebra.ssrint]
+intr_sign [in mathcomp.algebra.ssrint]
+intr_sg [in mathcomp.algebra.ssrint]
+intr_eq0 [in mathcomp.algebra.ssrint]
+intS [in mathcomp.algebra.ssrint]
+intUnitRing.idomain_axiomz [in mathcomp.algebra.ssrint]
+intUnitRing.invz_out [in mathcomp.algebra.ssrint]
+intUnitRing.mulVz [in mathcomp.algebra.ssrint]
+intUnitRing.mulzn_eq1 [in mathcomp.algebra.ssrint]
+intUnitRing.unitzPl [in mathcomp.algebra.ssrint]
+intz [in mathcomp.algebra.ssrint]
+intZmod.addNz [in mathcomp.algebra.ssrint]
+intZmod.addPz [in mathcomp.algebra.ssrint]
+intZmod.addSnz [in mathcomp.algebra.ssrint]
+intZmod.addSz [in mathcomp.algebra.ssrint]
+intZmod.addzA [in mathcomp.algebra.ssrint]
+intZmod.addzC [in mathcomp.algebra.ssrint]
+intZmod.add0z [in mathcomp.algebra.ssrint]
+intZmod.add1Pz [in mathcomp.algebra.ssrint]
+intZmod.intP [in mathcomp.algebra.ssrint]
+intZmod.int_rect [in mathcomp.algebra.ssrint]
+intZmod.NegzE [in mathcomp.algebra.ssrint]
+intZmod.oppzK [in mathcomp.algebra.ssrint]
+intZmod.oppz_add [in mathcomp.algebra.ssrint]
+intZmod.PoszD [in mathcomp.algebra.ssrint]
+intZmod.predn_int [in mathcomp.algebra.ssrint]
+intZmod.subSz1 [in mathcomp.algebra.ssrint]
+int_Smith_normal_form [in mathcomp.algebra.intdiv]
+int_rect [in mathcomp.algebra.ssrint]
+invariant_chief_irr_cases [in mathcomp.character.inertia]
+invariant_subnormal [in mathcomp.solvable.gseries]
+invariant_inj [in mathcomp.ssreflect.eqtype]
+invariant_comp [in mathcomp.ssreflect.eqtype]
+invCg [in mathcomp.fingroup.fingroup]
+invDg [in mathcomp.fingroup.fingroup]
+invF_f [in mathcomp.ssreflect.fintype]
+invGid [in mathcomp.fingroup.fingroup]
+invgK [in mathcomp.fingroup.fingroup]
+invg_expg [in mathcomp.fingroup.fingroup]
+invg_rcoset [in mathcomp.fingroup.fingroup]
+invg_lcoset [in mathcomp.fingroup.fingroup]
+invg_lcosets [in mathcomp.fingroup.fingroup]
+invg_set1 [in mathcomp.fingroup.fingroup]
+invg_comm [in mathcomp.fingroup.fingroup]
+invg_inj [in mathcomp.fingroup.fingroup]
+invg1 [in mathcomp.fingroup.fingroup]
+invg2id [in mathcomp.fingroup.fingroup]
+invIg [in mathcomp.fingroup.fingroup]
+invmE [in mathcomp.fingroup.morphism]
+invMG [in mathcomp.fingroup.fingroup]
+invMg [in mathcomp.fingroup.fingroup]
+invmK [in mathcomp.fingroup.morphism]
+invmxK [in mathcomp.algebra.matrix]
+invmxZ [in mathcomp.algebra.matrix]
+invmx_out [in mathcomp.algebra.matrix]
+invmx_scalar [in mathcomp.algebra.matrix]
+invmx1 [in mathcomp.algebra.matrix]
+invm_subker [in mathcomp.fingroup.morphism]
+involutions_gen_dihedral [in mathcomp.solvable.extremal]
+invq_frac [in mathcomp.algebra.rat]
+invq0 [in mathcomp.algebra.rat]
+invr_lin_char [in mathcomp.character.character]
+invr_expz [in mathcomp.algebra.ssrint]
+invSg [in mathcomp.fingroup.fingroup]
+invUg [in mathcomp.fingroup.fingroup]
+inv_is_ahom [in mathcomp.field.galois]
+inv_kHomf [in mathcomp.field.galois]
+inv_quotientN [in mathcomp.fingroup.quotient]
+inv_quotientS [in mathcomp.fingroup.quotient]
+inv_lfun_def [in mathcomp.algebra.vector]
+inv_dprod_Iirr0 [in mathcomp.character.character]
+inv_dprod_IirrK [in mathcomp.character.character]
+inv_eq [in mathcomp.ssreflect.eqtype]
+inv_subG [in mathcomp.fingroup.fingroup]
+in_factmod_module [in mathcomp.character.mxrepresentation]
+in_submod_module [in mathcomp.character.mxrepresentation]
+in_factmodJ [in mathcomp.character.mxrepresentation]
+in_submodJ [in mathcomp.character.mxrepresentation]
+in_factmodsK [in mathcomp.character.mxrepresentation]
+in_factmod_addsK [in mathcomp.character.mxrepresentation]
+in_factmodK [in mathcomp.character.mxrepresentation]
+in_factmod_eq0 [in mathcomp.character.mxrepresentation]
+in_factmodE [in mathcomp.character.mxrepresentation]
+in_submod_eq0 [in mathcomp.character.mxrepresentation]
+in_submodK [in mathcomp.character.mxrepresentation]
+in_submodE [in mathcomp.character.mxrepresentation]
+in_tupleE [in mathcomp.ssreflect.tuple]
+in_nil [in mathcomp.ssreflect.seq]
+in_cons [in mathcomp.ssreflect.seq]
+in_iinv_f [in mathcomp.ssreflect.fintype]
+in_cprodM [in mathcomp.solvable.center]
+in_setX [in mathcomp.ssreflect.finset]
+in_setD [in mathcomp.ssreflect.finset]
+in_setC [in mathcomp.ssreflect.finset]
+in_setI [in mathcomp.ssreflect.finset]
+in_setU [in mathcomp.ssreflect.finset]
+in_set2 [in mathcomp.ssreflect.finset]
+in_setD1 [in mathcomp.ssreflect.finset]
+in_setC1 [in mathcomp.ssreflect.finset]
+in_setU1 [in mathcomp.ssreflect.finset]
+in_set1 [in mathcomp.ssreflect.finset]
+in_set0 [in mathcomp.ssreflect.finset]
+in_setT [in mathcomp.ssreflect.finset]
+in_set [in mathcomp.ssreflect.finset]
+iota_ltn_sorted [in mathcomp.ssreflect.path]
+iota_sorted [in mathcomp.ssreflect.path]
+iota_tupleP [in mathcomp.ssreflect.tuple]
+iota_uniq [in mathcomp.ssreflect.seq]
+iota_addl [in mathcomp.ssreflect.seq]
+iota_add [in mathcomp.ssreflect.seq]
+irrEchar [in mathcomp.character.character]
+irredp_FAdjoin [in mathcomp.field.fieldext]
+irrK [in mathcomp.character.character]
+irrP [in mathcomp.character.character]
+irrRepr [in mathcomp.character.character]
+irrWchar [in mathcomp.character.character]
+irrWnorm [in mathcomp.character.character]
+irr_gring_center [in mathcomp.character.integral_char]
+irr_constt_to_dirr [in mathcomp.character.vcharacter]
+irr_dirr [in mathcomp.character.vcharacter]
+irr_vchar [in mathcomp.character.vcharacter]
+irr_vchar_on [in mathcomp.character.vcharacter]
+irr_modeV [in mathcomp.character.mxrepresentation]
+irr_mode_neq0 [in mathcomp.character.mxrepresentation]
+irr_mode_unit [in mathcomp.character.mxrepresentation]
+irr_modeX [in mathcomp.character.mxrepresentation]
+irr_modeM [in mathcomp.character.mxrepresentation]
+irr_center_scalar [in mathcomp.character.mxrepresentation]
+irr_mode1 [in mathcomp.character.mxrepresentation]
+irr_degree_abelian [in mathcomp.character.mxrepresentation]
+irr_mx_mult [in mathcomp.character.mxrepresentation]
+irr_comp_id [in mathcomp.character.mxrepresentation]
+irr_repr'_op0 [in mathcomp.character.mxrepresentation]
+irr_reprK [in mathcomp.character.mxrepresentation]
+irr_comp_rsim [in mathcomp.character.mxrepresentation]
+irr_comp_envelop [in mathcomp.character.mxrepresentation]
+irr_comp'_op0 [in mathcomp.character.mxrepresentation]
+irr_mx_sum [in mathcomp.character.mxrepresentation]
+irr_reprE [in mathcomp.character.mxrepresentation]
+irr_degree_gt0 [in mathcomp.character.mxrepresentation]
+irr_degreeE [in mathcomp.character.mxrepresentation]
+irr_faithful_center [in mathcomp.character.character]
+irr_cfcenterE [in mathcomp.character.character]
+irr_prime_injP [in mathcomp.character.character]
+irr_aut_closed [in mathcomp.character.character]
+irr_consttE [in mathcomp.character.character]
+irr_orthonormal [in mathcomp.character.character]
+irr_classK [in mathcomp.character.character]
+irr_classP [in mathcomp.character.character]
+irr_inv [in mathcomp.character.character]
+irr_prime_lin [in mathcomp.character.character]
+irr_cyclic_lin [in mathcomp.character.character]
+irr_repr_lin_char [in mathcomp.character.character]
+irr_char [in mathcomp.character.character]
+irr_reprP [in mathcomp.character.character]
+irr_basis [in mathcomp.character.character]
+irr_eq1 [in mathcomp.character.character]
+irr_inj [in mathcomp.character.character]
+irr_free [in mathcomp.character.character]
+irr_sum_square [in mathcomp.character.character]
+irr_neq0 [in mathcomp.character.character]
+irr_key [in mathcomp.character.character]
+irr_of_socle_bij [in mathcomp.character.character]
+irr_of_socleK [in mathcomp.character.character]
+irr_induced_Frobenius_ker [in mathcomp.character.inertia]
+irr0 [in mathcomp.character.character]
+irr1_mode [in mathcomp.character.mxrepresentation]
+irr1_repr [in mathcomp.character.mxrepresentation]
+irr1_rfix [in mathcomp.character.mxrepresentation]
+irr1_abelian_bound [in mathcomp.character.character]
+irr1_bound [in mathcomp.character.character]
+irr1_neq0 [in mathcomp.character.character]
+irr1_gt0 [in mathcomp.character.character]
+irr1_degree [in mathcomp.character.character]
+isgroupP [in mathcomp.fingroup.fingroup]
+isnullP [in mathcomp.field.closed_field]
+isnull_qf [in mathcomp.field.closed_field]
+isogEcard [in mathcomp.fingroup.morphism]
+isogEhom [in mathcomp.fingroup.morphism]
+isogP [in mathcomp.fingroup.morphism]
+isoGrpP [in mathcomp.fingroup.presentation]
+isoGrp_trans [in mathcomp.fingroup.presentation]
+isoGrp_hom [in mathcomp.fingroup.presentation]
+isog_pseries [in mathcomp.solvable.pgroup]
+isog_pcore [in mathcomp.solvable.pgroup]
+isog_pgroup [in mathcomp.solvable.pgroup]
+isog_dprod [in mathcomp.fingroup.gproduct]
+isog_set1X [in mathcomp.fingroup.gproduct]
+isog_setX1 [in mathcomp.fingroup.gproduct]
+isog_2extraspecial [in mathcomp.solvable.extraspecial]
+isog_2X1p2 [in mathcomp.solvable.extraspecial]
+isog_pX1p2n [in mathcomp.solvable.extraspecial]
+isog_pX1p2 [in mathcomp.solvable.extraspecial]
+isog_homocyclic [in mathcomp.solvable.abelian]
+isog_abelem_card [in mathcomp.solvable.abelian]
+isog_abelian_type [in mathcomp.solvable.abelian]
+isog_Mho [in mathcomp.solvable.abelian]
+isog_Ohm [in mathcomp.solvable.abelian]
+isog_rank [in mathcomp.solvable.abelian]
+isog_p_rank [in mathcomp.solvable.abelian]
+isog_grank [in mathcomp.solvable.abelian]
+isog_abelem [in mathcomp.solvable.abelian]
+isog_simple [in mathcomp.solvable.gseries]
+isog_extraspecial [in mathcomp.solvable.maximal]
+isog_special [in mathcomp.solvable.maximal]
+isog_Fitting [in mathcomp.solvable.maximal]
+isog_Phi [in mathcomp.solvable.maximal]
+isog_abelem_rV [in mathcomp.character.mxabelem]
+isog_sol [in mathcomp.solvable.nilpotent]
+isog_nil_class [in mathcomp.solvable.nilpotent]
+isog_nil [in mathcomp.solvable.nilpotent]
+isog_der [in mathcomp.solvable.commutator]
+isog_subg [in mathcomp.fingroup.morphism]
+isog_hom [in mathcomp.fingroup.morphism]
+isog_transr [in mathcomp.fingroup.morphism]
+isog_transl [in mathcomp.fingroup.morphism]
+isog_sym [in mathcomp.fingroup.morphism]
+isog_trans [in mathcomp.fingroup.morphism]
+isog_symr [in mathcomp.fingroup.morphism]
+isog_eq1 [in mathcomp.fingroup.morphism]
+isog_abelian [in mathcomp.fingroup.morphism]
+isog_refl [in mathcomp.fingroup.morphism]
+isog_isom [in mathcomp.fingroup.morphism]
+isog_xcprod [in mathcomp.solvable.center]
+isog_cprod_by [in mathcomp.solvable.center]
+isog_center [in mathcomp.solvable.center]
+isog_cyclic_card [in mathcomp.solvable.cyclic]
+isog_cyclic [in mathcomp.solvable.cyclic]
+isometries_iso [in mathcomp.solvable.burnside_app]
+isometry_in_zchar [in mathcomp.character.vcharacter]
+isometry_raddf_inj [in mathcomp.character.classfun]
+isometry_of_cfnorm [in mathcomp.character.classfun]
+isometry_of_free [in mathcomp.character.classfun]
+isomP [in mathcomp.fingroup.morphism]
+isom_IirrKV [in mathcomp.character.character]
+isom_IirrK [in mathcomp.character.character]
+isom_Iirr0 [in mathcomp.character.character]
+isom_Iirr_eq0 [in mathcomp.character.character]
+isom_Iirr_inj [in mathcomp.character.character]
+isom_IirrE [in mathcomp.character.character]
+isom_restr_perm [in mathcomp.fingroup.action]
+isom_sgval [in mathcomp.fingroup.morphism]
+isom_subg [in mathcomp.fingroup.morphism]
+isom_sym [in mathcomp.fingroup.morphism]
+isom_sub_im [in mathcomp.fingroup.morphism]
+isom_card [in mathcomp.fingroup.morphism]
+isom_im [in mathcomp.fingroup.morphism]
+isom_inj [in mathcomp.fingroup.morphism]
+isom_isog [in mathcomp.fingroup.morphism]
+iso_eq_F0_F1_F2 [in mathcomp.solvable.burnside_app]
+iso_eq_F0_F1 [in mathcomp.solvable.burnside_app]
+iso0_1 [in mathcomp.solvable.burnside_app]
+iso3_ndir [in mathcomp.solvable.burnside_app]
+isSome_insub [in mathcomp.ssreflect.eqtype]
+is_perm_mxV [in mathcomp.algebra.matrix]
+is_perm_mxMr [in mathcomp.algebra.matrix]
+is_perm_mx_tr [in mathcomp.algebra.matrix]
+is_perm_mxMl [in mathcomp.algebra.matrix]
+is_perm_mx1 [in mathcomp.algebra.matrix]
+is_perm_mxP [in mathcomp.algebra.matrix]
+is_scalar_mxP [in mathcomp.algebra.matrix]
+is_abelemP [in mathcomp.solvable.abelian]
+is_abelem_pgroup [in mathcomp.solvable.abelian]
+is_total_action [in mathcomp.fingroup.action]
+is_iso3P [in mathcomp.solvable.burnside_app]
+is_isoP [in mathcomp.solvable.burnside_app]
+iteriS [in mathcomp.ssreflect.ssrnat]
+iteropS [in mathcomp.ssreflect.ssrnat]
+iterS [in mathcomp.ssreflect.ssrnat]
+iterSr [in mathcomp.ssreflect.ssrnat]
+iter_pcycle [in mathcomp.fingroup.perm]
+iter_muln_1 [in mathcomp.ssreflect.ssrnat]
+iter_muln [in mathcomp.ssreflect.ssrnat]
+iter_addn_0 [in mathcomp.ssreflect.ssrnat]
+iter_addn [in mathcomp.ssreflect.ssrnat]
+iter_predn [in mathcomp.ssreflect.ssrnat]
+iter_succn_0 [in mathcomp.ssreflect.ssrnat]
+iter_succn [in mathcomp.ssreflect.ssrnat]
+iter_add [in mathcomp.ssreflect.ssrnat]
+iter_finv [in mathcomp.ssreflect.fingraph]
+iter_order [in mathcomp.ssreflect.fingraph]
+iter_finv_in [in mathcomp.ssreflect.fingraph]
+iter_order_in [in mathcomp.ssreflect.fingraph]
+iter_in [in mathcomp.ssreflect.fingraph]
+iter_findex [in mathcomp.ssreflect.fingraph]
+itvP [in mathcomp.algebra.interval]
+itv_splitU2 [in mathcomp.algebra.interval]
+itv_splitU [in mathcomp.algebra.interval]
+itv_splitI [in mathcomp.algebra.interval]
+itv_gte [in mathcomp.algebra.interval]
+itv_xx [in mathcomp.algebra.interval]
+itv_boundlr [in mathcomp.algebra.interval]
+itv_dec [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) | +