| 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) | -
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_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]
-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 | -(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) | -