| 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) | +
Q
+qact [definition, in mathcomp.fingroup.action]+qactE [lemma, in mathcomp.fingroup.action]
+qactEcond [lemma, in mathcomp.fingroup.action]
+qactJ [lemma, in mathcomp.fingroup.action]
+qacts_coset [lemma, in mathcomp.solvable.jordanholder]
+qacts_cosetpre [lemma, in mathcomp.solvable.jordanholder]
+qact_dom_doms [lemma, in mathcomp.solvable.jordanholder]
+qact_domE [lemma, in mathcomp.fingroup.action]
+qact_is_groupAction [lemma, in mathcomp.fingroup.action]
+qact_proof [lemma, in mathcomp.fingroup.action]
+qact_subdomE [lemma, in mathcomp.fingroup.action]
+qact_dom [definition, in mathcomp.fingroup.action]
+QEdecFieldMixin [abbreviation, in mathcomp.algebra.ssralg]
+qf [abbreviation, in mathcomp.field.closed_field]
+qf_eval [abbreviation, in mathcomp.character.mxrepresentation]
+qf_form [abbreviation, in mathcomp.character.mxrepresentation]
+Qint [definition, in mathcomp.algebra.rat]
+QintP [lemma, in mathcomp.algebra.rat]
+QintPred [section, in mathcomp.algebra.rat]
+Qint_subring_closed [lemma, in mathcomp.algebra.rat]
+Qint_def [lemma, in mathcomp.algebra.rat]
+Qint_key [lemma, in mathcomp.algebra.rat]
+Qint_dvdz [lemma, in mathcomp.algebra.intdiv]
+qisom [definition, in mathcomp.fingroup.quotient]
+qisomE [lemma, in mathcomp.fingroup.quotient]
+qisom_inj [lemma, in mathcomp.fingroup.quotient]
+qisom_isog [lemma, in mathcomp.fingroup.quotient]
+qisom_isom [lemma, in mathcomp.fingroup.quotient]
+qisom_restr_proof [lemma, in mathcomp.fingroup.quotient]
+qisom_ker_proof [lemma, in mathcomp.fingroup.quotient]
+Qmorphism [abbreviation, in mathcomp.field.algebraics_fundamentals]
+Qnat [definition, in mathcomp.algebra.rat]
+QnatP [lemma, in mathcomp.algebra.rat]
+QnatPred [section, in mathcomp.algebra.rat]
+Qnat_semiring_closed [lemma, in mathcomp.algebra.rat]
+Qnat_def [lemma, in mathcomp.algebra.rat]
+Qnat_key [lemma, in mathcomp.algebra.rat]
+Qnat_dvd [lemma, in mathcomp.algebra.intdiv]
+Qn_aut_exists [lemma, in mathcomp.field.algnum]
+QtoC [abbreviation, in mathcomp.field.algC]
+QtoC [abbreviation, in mathcomp.field.cyclotomic]
+QtoC [abbreviation, in mathcomp.field.algnum]
+QtoCm [abbreviation, in mathcomp.field.algC]
+QtoCm [abbreviation, in mathcomp.field.algnum]
+QtoC_M [abbreviation, in mathcomp.field.cyclotomic]
+QuantifierCombinators [section, in mathcomp.ssreflect.fintype]
+QuantifierCombinators.P [variable, in mathcomp.ssreflect.fintype]
+QuantifierCombinators.PP [variable, in mathcomp.ssreflect.fintype]
+QuantifierCombinators.T [variable, in mathcomp.ssreflect.fintype]
+QuantifierCombinators.viewP [variable, in mathcomp.ssreflect.fintype]
+Quantifiers [section, in mathcomp.ssreflect.fintype]
+Quantifiers.rT [variable, in mathcomp.ssreflect.fintype]
+Quantifiers.T [variable, in mathcomp.ssreflect.fintype]
+Quaternion [constructor, in mathcomp.solvable.extremal]
+quaternion_classP [lemma, in mathcomp.solvable.extremal]
+quaternion_structure [lemma, in mathcomp.solvable.extremal]
+quaternion_gtype [definition, in mathcomp.solvable.extremal]
+quaternion_kernel [definition, in mathcomp.solvable.extremal]
+QuoMax [section, in mathcomp.solvable.gseries]
+QuoMax.G [variable, in mathcomp.solvable.gseries]
+QuoMax.gT [variable, in mathcomp.solvable.gseries]
+QuoMax.H [variable, in mathcomp.solvable.gseries]
+QuoMax.K [variable, in mathcomp.solvable.gseries]
+QuotClass [constructor, in mathcomp.ssreflect.generic_quotient]
+quotient [definition, in mathcomp.fingroup.quotient]
+Quotient [module, in mathcomp.algebra.ring_quotient]
+quotient [library]
+QuotientAbelem [section, in mathcomp.solvable.abelian]
+QuotientAbelem.gT [variable, in mathcomp.solvable.abelian]
+QuotientAbelem.p [variable, in mathcomp.solvable.abelian]
+QuotientAction [section, in mathcomp.fingroup.action]
+QuotientAction.aT [variable, in mathcomp.fingroup.action]
+QuotientAction.D [variable, in mathcomp.fingroup.action]
+QuotientAction.H [variable, in mathcomp.fingroup.action]
+QuotientAction.rT [variable, in mathcomp.fingroup.action]
+QuotientAction.to [variable, in mathcomp.fingroup.action]
+quotientD [lemma, in mathcomp.fingroup.quotient]
+QuotientDef [section, in mathcomp.ssreflect.generic_quotient]
+QuotientDef.qT [variable, in mathcomp.ssreflect.generic_quotient]
+QuotientDef.T [variable, in mathcomp.ssreflect.generic_quotient]
+\pi [notation, in mathcomp.ssreflect.generic_quotient]
+quotientDG [lemma, in mathcomp.fingroup.quotient]
+quotientD1 [lemma, in mathcomp.fingroup.quotient]
+quotientE [lemma, in mathcomp.fingroup.quotient]
+quotientGI [lemma, in mathcomp.fingroup.quotient]
+quotientGK [lemma, in mathcomp.fingroup.quotient]
+quotientI [lemma, in mathcomp.fingroup.quotient]
+quotientIG [lemma, in mathcomp.fingroup.quotient]
+quotientInorm [lemma, in mathcomp.fingroup.quotient]
+QuotientInternalProd [section, in mathcomp.fingroup.gproduct]
+QuotientInternalProd.G [variable, in mathcomp.fingroup.gproduct]
+QuotientInternalProd.gT [variable, in mathcomp.fingroup.gproduct]
+QuotientInternalProd.H [variable, in mathcomp.fingroup.gproduct]
+QuotientInternalProd.K [variable, in mathcomp.fingroup.gproduct]
+QuotientInternalProd.M [variable, in mathcomp.fingroup.gproduct]
+QuotientInternalProd.nMG [variable, in mathcomp.fingroup.gproduct]
+quotientJ [lemma, in mathcomp.fingroup.quotient]
+quotientK [lemma, in mathcomp.fingroup.quotient]
+quotientMidl [lemma, in mathcomp.fingroup.quotient]
+quotientMidr [lemma, in mathcomp.fingroup.quotient]
+quotientMl [lemma, in mathcomp.fingroup.quotient]
+QuotientMorphism [section, in mathcomp.fingroup.quotient]
+QuotientMorphism.f [variable, in mathcomp.fingroup.quotient]
+QuotientMorphism.G [variable, in mathcomp.fingroup.quotient]
+QuotientMorphism.gT [variable, in mathcomp.fingroup.quotient]
+QuotientMorphism.H [variable, in mathcomp.fingroup.quotient]
+QuotientMorphism.nfHfG [variable, in mathcomp.fingroup.quotient]
+QuotientMorphism.nHG [variable, in mathcomp.fingroup.quotient]
+QuotientMorphism.nsHG [variable, in mathcomp.fingroup.quotient]
+QuotientMorphism.rT [variable, in mathcomp.fingroup.quotient]
+QuotientMorphism.sHG [variable, in mathcomp.fingroup.quotient]
+quotientMr [lemma, in mathcomp.fingroup.quotient]
+QuotientNil [section, in mathcomp.solvable.nilpotent]
+QuotientNil.gT [variable, in mathcomp.solvable.nilpotent]
+quotientR [lemma, in mathcomp.fingroup.quotient]
+QuotientRank [section, in mathcomp.solvable.abelian]
+QuotientRank.cGG [variable, in mathcomp.solvable.abelian]
+QuotientRank.G [variable, in mathcomp.solvable.abelian]
+QuotientRank.gT [variable, in mathcomp.solvable.abelian]
+QuotientRank.H [variable, in mathcomp.solvable.abelian]
+QuotientRank.p [variable, in mathcomp.solvable.abelian]
+quotientS [lemma, in mathcomp.fingroup.quotient]
+quotientSGK [lemma, in mathcomp.fingroup.quotient]
+quotientSK [lemma, in mathcomp.fingroup.quotient]
+QuotientSol [section, in mathcomp.solvable.nilpotent]
+QuotientSol.gT [variable, in mathcomp.solvable.nilpotent]
+QuotientSol.rT [variable, in mathcomp.solvable.nilpotent]
+quotientS1 [lemma, in mathcomp.fingroup.quotient]
+quotientT [lemma, in mathcomp.fingroup.quotient]
+quotientU [lemma, in mathcomp.fingroup.quotient]
+quotientV [lemma, in mathcomp.fingroup.quotient]
+quotientY [lemma, in mathcomp.fingroup.quotient]
+quotientYidl [lemma, in mathcomp.fingroup.quotient]
+quotientYidr [lemma, in mathcomp.fingroup.quotient]
+quotientYK [lemma, in mathcomp.fingroup.quotient]
+quotient_TI_subcent [lemma, in mathcomp.solvable.hall]
+quotient_pseries_cat [lemma, in mathcomp.solvable.pgroup]
+quotient_pseries2 [lemma, in mathcomp.solvable.pgroup]
+quotient_pseries [lemma, in mathcomp.solvable.pgroup]
+quotient_pcore_mod [lemma, in mathcomp.solvable.pgroup]
+quotient_odd [lemma, in mathcomp.solvable.pgroup]
+quotient_pHall [lemma, in mathcomp.solvable.pgroup]
+quotient_pgroup [lemma, in mathcomp.solvable.pgroup]
+quotient_isog [lemma, in mathcomp.fingroup.quotient]
+quotient_isom [lemma, in mathcomp.fingroup.quotient]
+quotient_subnormG [lemma, in mathcomp.fingroup.quotient]
+quotient_normG [lemma, in mathcomp.fingroup.quotient]
+quotient_subcent [lemma, in mathcomp.fingroup.quotient]
+quotient_abelian [lemma, in mathcomp.fingroup.quotient]
+quotient_cents [lemma, in mathcomp.fingroup.quotient]
+quotient_cent [lemma, in mathcomp.fingroup.quotient]
+quotient_subcent1 [lemma, in mathcomp.fingroup.quotient]
+quotient_cent1s [lemma, in mathcomp.fingroup.quotient]
+quotient_cent1 [lemma, in mathcomp.fingroup.quotient]
+quotient_normal [lemma, in mathcomp.fingroup.quotient]
+quotient_subnorm [lemma, in mathcomp.fingroup.quotient]
+quotient_norms [lemma, in mathcomp.fingroup.quotient]
+quotient_norm [lemma, in mathcomp.fingroup.quotient]
+quotient_gen [lemma, in mathcomp.fingroup.quotient]
+quotient_neq1 [lemma, in mathcomp.fingroup.quotient]
+quotient_inj [lemma, in mathcomp.fingroup.quotient]
+quotient_injG [lemma, in mathcomp.fingroup.quotient]
+quotient_sub1 [lemma, in mathcomp.fingroup.quotient]
+quotient_proper [lemma, in mathcomp.fingroup.quotient]
+quotient_class [lemma, in mathcomp.fingroup.quotient]
+quotient_homg [lemma, in mathcomp.fingroup.quotient]
+quotient_set1 [lemma, in mathcomp.fingroup.quotient]
+quotient_setIpre [lemma, in mathcomp.fingroup.quotient]
+quotient_splitting_field [lemma, in mathcomp.character.mxrepresentation]
+quotient_coprime_dprod [lemma, in mathcomp.fingroup.gproduct]
+quotient_cprod [lemma, in mathcomp.fingroup.gproduct]
+quotient_coprime_sdprod [lemma, in mathcomp.fingroup.gproduct]
+quotient_pprod [lemma, in mathcomp.fingroup.gproduct]
+quotient_sdprodr_isog [lemma, in mathcomp.fingroup.gproduct]
+quotient_sdprodr_isom [lemma, in mathcomp.fingroup.gproduct]
+quotient_p_rank_abelian [lemma, in mathcomp.solvable.abelian]
+quotient_rank_abelian [lemma, in mathcomp.solvable.abelian]
+quotient_grank [lemma, in mathcomp.solvable.abelian]
+quotient_pnElem [lemma, in mathcomp.solvable.abelian]
+quotient_pElem [lemma, in mathcomp.solvable.abelian]
+quotient_abelem [lemma, in mathcomp.solvable.abelian]
+quotient_Ldiv [lemma, in mathcomp.solvable.abelian]
+quotient_LdivT [lemma, in mathcomp.solvable.abelian]
+quotient_simple [lemma, in mathcomp.solvable.gseries]
+quotient_maximal_eq [lemma, in mathcomp.solvable.gseries]
+quotient_maximal [lemma, in mathcomp.solvable.gseries]
+quotient_subnormal [lemma, in mathcomp.solvable.gseries]
+quotient_Phi [lemma, in mathcomp.solvable.maximal]
+quotient_astabQ [lemma, in mathcomp.fingroup.action]
+quotient_cfker_mod [lemma, in mathcomp.character.classfun]
+quotient_sol [lemma, in mathcomp.solvable.nilpotent]
+quotient_center_nil [lemma, in mathcomp.solvable.nilpotent]
+quotient_nil [lemma, in mathcomp.solvable.nilpotent]
+quotient_ucn_add [lemma, in mathcomp.solvable.nilpotent]
+quotient_der [lemma, in mathcomp.solvable.commutator]
+quotient_cents2r [lemma, in mathcomp.solvable.commutator]
+quotient_cents2 [lemma, in mathcomp.solvable.commutator]
+quotient_generator [lemma, in mathcomp.solvable.cyclic]
+quotient_cyclic [lemma, in mathcomp.solvable.cyclic]
+quotient_cycle [lemma, in mathcomp.solvable.cyclic]
+Quotient.add [definition, in mathcomp.algebra.ring_quotient]
+Quotient.addNq [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.addqA [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.addqC [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.add0q [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.equiv [definition, in mathcomp.algebra.ring_quotient]
+Quotient.equivE [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.equiv_is_equiv [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.idealrBE [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.idealrDE [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.IDomainQuotient [section, in mathcomp.algebra.ring_quotient]
+Quotient.IDomainQuotient.I [variable, in mathcomp.algebra.ring_quotient]
+Quotient.IDomainQuotient.kI [variable, in mathcomp.algebra.ring_quotient]
+Quotient.IDomainQuotient.pidealI [variable, in mathcomp.algebra.ring_quotient]
+Quotient.IDomainQuotient.R [variable, in mathcomp.algebra.ring_quotient]
+Quotient.mul [definition, in mathcomp.algebra.ring_quotient]
+Quotient.mulqA [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.mulqC [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.mulq_addl [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.mul1q [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.nonzero1q [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.one [definition, in mathcomp.algebra.ring_quotient]
+Quotient.opp [definition, in mathcomp.algebra.ring_quotient]
+Quotient.pi_mul [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.pi_add [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.pi_opp [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.RingQuotient [section, in mathcomp.algebra.ring_quotient]
+Quotient.RingQuotient.I [variable, in mathcomp.algebra.ring_quotient]
+Quotient.RingQuotient.idealI [variable, in mathcomp.algebra.ring_quotient]
+Quotient.RingQuotient.kI [variable, in mathcomp.algebra.ring_quotient]
+Quotient.RingQuotient.R [variable, in mathcomp.algebra.ring_quotient]
+Quotient.rquot_IdomainAxiom [lemma, in mathcomp.algebra.ring_quotient]
+Quotient.rquot_ringQuotMixin [definition, in mathcomp.algebra.ring_quotient]
+Quotient.rquot_comRingMixin [definition, in mathcomp.algebra.ring_quotient]
+Quotient.rquot_zmodQuotMixin [definition, in mathcomp.algebra.ring_quotient]
+Quotient.rquot_zmodMixin [definition, in mathcomp.algebra.ring_quotient]
+Quotient.type [abbreviation, in mathcomp.algebra.ring_quotient]
+Quotient.type [definition, in mathcomp.algebra.ring_quotient]
+Quotient.type_of [definition, in mathcomp.algebra.ring_quotient]
+Quotient.zero [definition, in mathcomp.algebra.ring_quotient]
+Quotient.ZmodQuotient [section, in mathcomp.algebra.ring_quotient]
+Quotient.ZmodQuotient.I [variable, in mathcomp.algebra.ring_quotient]
+Quotient.ZmodQuotient.kI [variable, in mathcomp.algebra.ring_quotient]
+Quotient.ZmodQuotient.R [variable, in mathcomp.algebra.ring_quotient]
+Quotient.ZmodQuotient.zmodI [variable, in mathcomp.algebra.ring_quotient]
+{quot _ } [notation, in mathcomp.algebra.ring_quotient]
+quotient0 [lemma, in mathcomp.fingroup.quotient]
+Quotient1 [section, in mathcomp.fingroup.quotient]
+quotient1 [lemma, in mathcomp.fingroup.quotient]
+quotient1_isog [lemma, in mathcomp.fingroup.quotient]
+quotient1_isom [lemma, in mathcomp.fingroup.quotient]
+Quotient1.A [variable, in mathcomp.fingroup.quotient]
+Quotient1.gT [variable, in mathcomp.fingroup.quotient]
+quotm [definition, in mathcomp.fingroup.quotient]
+quotmE [lemma, in mathcomp.fingroup.quotient]
+quotm_ker_proof [lemma, in mathcomp.fingroup.quotient]
+quotm_dom_proof [lemma, in mathcomp.fingroup.quotient]
+quotP [lemma, in mathcomp.ssreflect.generic_quotient]
+QuotSubType [module, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.choiceMixin [definition, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.countMixin [definition, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.eqMixin [definition, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.finMixin [definition, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.finType [section, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.finType.qT [variable, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.finType.T [variable, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.qreprK [lemma, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.reprP [lemma, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.sortPx [lemma, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.sort_Sub [lemma, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.Sub [definition, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.SubTypeMixin [section, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.SubTypeMixin.qT [variable, in mathcomp.ssreflect.generic_quotient]
+QuotSubType.SubTypeMixin.T [variable, in mathcomp.ssreflect.generic_quotient]
+QuotType [abbreviation, in mathcomp.ssreflect.generic_quotient]
+quotType [record, in mathcomp.ssreflect.generic_quotient]
+QuotTypePack [constructor, in mathcomp.ssreflect.generic_quotient]
+QuotTypeTheory [section, in mathcomp.ssreflect.generic_quotient]
+QuotTypeTheory.qT [variable, in mathcomp.ssreflect.generic_quotient]
+QuotTypeTheory.T [variable, in mathcomp.ssreflect.generic_quotient]
+QuotType_clone [definition, in mathcomp.ssreflect.generic_quotient]
+QuotType_pack [definition, in mathcomp.ssreflect.generic_quotient]
+quotW [lemma, in mathcomp.ssreflect.generic_quotient]
+quot_class_of [abbreviation, in mathcomp.ssreflect.generic_quotient]
+quot_class [projection, in mathcomp.ssreflect.generic_quotient]
+quot_sort [projection, in mathcomp.ssreflect.generic_quotient]
+quot_class_of [abbreviation, in mathcomp.ssreflect.generic_quotient]
+quot_pi [projection, in mathcomp.ssreflect.generic_quotient]
+quot_repr [projection, in mathcomp.ssreflect.generic_quotient]
+quot_mixin_of [record, in mathcomp.ssreflect.generic_quotient]
+quo_mx_irr [lemma, in mathcomp.character.mxrepresentation]
+quo_mx_quotient [lemma, in mathcomp.character.mxrepresentation]
+quo_repr_coset [lemma, in mathcomp.character.mxrepresentation]
+quo_mx_repr [lemma, in mathcomp.character.mxrepresentation]
+quo_mx_coset [lemma, in mathcomp.character.mxrepresentation]
+quo_mx [definition, in mathcomp.character.mxrepresentation]
+quo_IirrKeq [lemma, in mathcomp.character.character]
+quo_IirrK [lemma, in mathcomp.character.character]
+quo_Iirr_eq0 [lemma, in mathcomp.character.character]
+quo_IirrE [lemma, in mathcomp.character.character]
+quo_Iirr0 [lemma, in mathcomp.character.character]
+quo_Iirr [definition, in mathcomp.character.character]
+Q8_extraspecial [lemma, in mathcomp.solvable.extraspecial]
+
| 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) | +