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 (75489 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 (1813 entries)
Binder 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 (45320 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 (382 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 (3967 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 (91 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 (14046 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 (469 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 (128 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 (457 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 (1372 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 (1025 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 (6124 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 (250 entries)

Q (lemma)

qactE [in mathcomp.fingroup.action]
qactEcond [in mathcomp.fingroup.action]
qactJ [in mathcomp.fingroup.action]
qacts_coset [in mathcomp.solvable.jordanholder]
qacts_cosetpre [in mathcomp.solvable.jordanholder]
qact_dom_doms [in mathcomp.solvable.jordanholder]
qact_domE [in mathcomp.fingroup.action]
qact_is_groupAction [in mathcomp.fingroup.action]
qact_proof [in mathcomp.fingroup.action]
qact_subdomE [in mathcomp.fingroup.action]
QintP [in mathcomp.algebra.rat]
Qint_dvdz [in mathcomp.algebra.intdiv]
Qint_subring_closed [in mathcomp.algebra.rat]
Qint_def [in mathcomp.algebra.rat]
Qint_key [in mathcomp.algebra.rat]
qisomE [in mathcomp.fingroup.quotient]
qisom_inj [in mathcomp.fingroup.quotient]
qisom_isog [in mathcomp.fingroup.quotient]
qisom_isom [in mathcomp.fingroup.quotient]
qisom_restr_proof [in mathcomp.fingroup.quotient]
qisom_ker_proof [in mathcomp.fingroup.quotient]
QnatP [in mathcomp.algebra.rat]
Qnat_dvd [in mathcomp.algebra.intdiv]
Qnat_semiring_closed [in mathcomp.algebra.rat]
Qnat_def [in mathcomp.algebra.rat]
Qnat_key [in mathcomp.algebra.rat]
Qn_aut_exists [in mathcomp.field.algnum]
quaternion_classP [in mathcomp.solvable.extremal]
quaternion_structure [in mathcomp.solvable.extremal]
quotientD [in mathcomp.fingroup.quotient]
quotientDG [in mathcomp.fingroup.quotient]
quotientD1 [in mathcomp.fingroup.quotient]
quotientE [in mathcomp.fingroup.quotient]
quotientGI [in mathcomp.fingroup.quotient]
quotientGK [in mathcomp.fingroup.quotient]
quotientI [in mathcomp.fingroup.quotient]
quotientIG [in mathcomp.fingroup.quotient]
quotientInorm [in mathcomp.fingroup.quotient]
quotientJ [in mathcomp.fingroup.quotient]
quotientK [in mathcomp.fingroup.quotient]
quotientMidl [in mathcomp.fingroup.quotient]
quotientMidr [in mathcomp.fingroup.quotient]
quotientMl [in mathcomp.fingroup.quotient]
quotientMr [in mathcomp.fingroup.quotient]
quotientR [in mathcomp.fingroup.quotient]
quotientS [in mathcomp.fingroup.quotient]
quotientSGK [in mathcomp.fingroup.quotient]
quotientSK [in mathcomp.fingroup.quotient]
quotientS1 [in mathcomp.fingroup.quotient]
quotientT [in mathcomp.fingroup.quotient]
quotientU [in mathcomp.fingroup.quotient]
quotientV [in mathcomp.fingroup.quotient]
quotientY [in mathcomp.fingroup.quotient]
quotientYidl [in mathcomp.fingroup.quotient]
quotientYidr [in mathcomp.fingroup.quotient]
quotientYK [in mathcomp.fingroup.quotient]
quotient_isog [in mathcomp.fingroup.quotient]
quotient_isom [in mathcomp.fingroup.quotient]
quotient_subnormG [in mathcomp.fingroup.quotient]
quotient_normG [in mathcomp.fingroup.quotient]
quotient_subcent [in mathcomp.fingroup.quotient]
quotient_abelian [in mathcomp.fingroup.quotient]
quotient_cents [in mathcomp.fingroup.quotient]
quotient_cent [in mathcomp.fingroup.quotient]
quotient_subcent1 [in mathcomp.fingroup.quotient]
quotient_cent1s [in mathcomp.fingroup.quotient]
quotient_cent1 [in mathcomp.fingroup.quotient]
quotient_normal [in mathcomp.fingroup.quotient]
quotient_subnorm [in mathcomp.fingroup.quotient]
quotient_norms [in mathcomp.fingroup.quotient]
quotient_norm [in mathcomp.fingroup.quotient]
quotient_gen [in mathcomp.fingroup.quotient]
quotient_neq1 [in mathcomp.fingroup.quotient]
quotient_inj [in mathcomp.fingroup.quotient]
quotient_injG [in mathcomp.fingroup.quotient]
quotient_sub1 [in mathcomp.fingroup.quotient]
quotient_proper [in mathcomp.fingroup.quotient]
quotient_class [in mathcomp.fingroup.quotient]
quotient_homg [in mathcomp.fingroup.quotient]
quotient_set1 [in mathcomp.fingroup.quotient]
quotient_setIpre [in mathcomp.fingroup.quotient]
quotient_der [in mathcomp.solvable.commutator]
quotient_cents2r [in mathcomp.solvable.commutator]
quotient_cents2 [in mathcomp.solvable.commutator]
quotient_astabQ [in mathcomp.fingroup.action]
quotient_cfker_mod [in mathcomp.character.classfun]
quotient_pseries_cat [in mathcomp.solvable.pgroup]
quotient_pseries2 [in mathcomp.solvable.pgroup]
quotient_pseries [in mathcomp.solvable.pgroup]
quotient_pcore_mod [in mathcomp.solvable.pgroup]
quotient_odd [in mathcomp.solvable.pgroup]
quotient_pHall [in mathcomp.solvable.pgroup]
quotient_pgroup [in mathcomp.solvable.pgroup]
quotient_splitting_field [in mathcomp.character.mxrepresentation]
quotient_coprime_dprod [in mathcomp.fingroup.gproduct]
quotient_cprod [in mathcomp.fingroup.gproduct]
quotient_coprime_sdprod [in mathcomp.fingroup.gproduct]
quotient_pprod [in mathcomp.fingroup.gproduct]
quotient_sdprodr_isog [in mathcomp.fingroup.gproduct]
quotient_sdprodr_isom [in mathcomp.fingroup.gproduct]
quotient_p_rank_abelian [in mathcomp.solvable.abelian]
quotient_rank_abelian [in mathcomp.solvable.abelian]
quotient_grank [in mathcomp.solvable.abelian]
quotient_pnElem [in mathcomp.solvable.abelian]
quotient_pElem [in mathcomp.solvable.abelian]
quotient_abelem [in mathcomp.solvable.abelian]
quotient_Ldiv [in mathcomp.solvable.abelian]
quotient_LdivT [in mathcomp.solvable.abelian]
quotient_simple [in mathcomp.solvable.gseries]
quotient_maximal_eq [in mathcomp.solvable.gseries]
quotient_maximal [in mathcomp.solvable.gseries]
quotient_subnormal [in mathcomp.solvable.gseries]
quotient_generator [in mathcomp.solvable.cyclic]
quotient_cyclic [in mathcomp.solvable.cyclic]
quotient_cycle [in mathcomp.solvable.cyclic]
quotient_TI_subcent [in mathcomp.solvable.hall]
quotient_Phi [in mathcomp.solvable.maximal]
quotient_sol [in mathcomp.solvable.nilpotent]
quotient_center_nil [in mathcomp.solvable.nilpotent]
quotient_nil [in mathcomp.solvable.nilpotent]
quotient_ucn_add [in mathcomp.solvable.nilpotent]
Quotient.addNq [in mathcomp.algebra.ring_quotient]
Quotient.addqA [in mathcomp.algebra.ring_quotient]
Quotient.addqC [in mathcomp.algebra.ring_quotient]
Quotient.add0q [in mathcomp.algebra.ring_quotient]
Quotient.equivE [in mathcomp.algebra.ring_quotient]
Quotient.equiv_is_equiv [in mathcomp.algebra.ring_quotient]
Quotient.idealrBE [in mathcomp.algebra.ring_quotient]
Quotient.idealrDE [in mathcomp.algebra.ring_quotient]
Quotient.mulqA [in mathcomp.algebra.ring_quotient]
Quotient.mulqC [in mathcomp.algebra.ring_quotient]
Quotient.mulq_addl [in mathcomp.algebra.ring_quotient]
Quotient.mul1q [in mathcomp.algebra.ring_quotient]
Quotient.nonzero1q [in mathcomp.algebra.ring_quotient]
Quotient.pi_mul [in mathcomp.algebra.ring_quotient]
Quotient.pi_add [in mathcomp.algebra.ring_quotient]
Quotient.pi_opp [in mathcomp.algebra.ring_quotient]
Quotient.rquot_IdomainAxiom [in mathcomp.algebra.ring_quotient]
quotient0 [in mathcomp.fingroup.quotient]
quotient1 [in mathcomp.fingroup.quotient]
quotient1_isog [in mathcomp.fingroup.quotient]
quotient1_isom [in mathcomp.fingroup.quotient]
quotmE [in mathcomp.fingroup.quotient]
quotm_ker_proof [in mathcomp.fingroup.quotient]
quotm_dom_proof [in mathcomp.fingroup.quotient]
quotP [in mathcomp.ssreflect.generic_quotient]
QuotSubType.qreprK [in mathcomp.ssreflect.generic_quotient]
QuotSubType.reprP [in mathcomp.ssreflect.generic_quotient]
QuotSubType.sortPx [in mathcomp.ssreflect.generic_quotient]
QuotSubType.sort_Sub [in mathcomp.ssreflect.generic_quotient]
quotW [in mathcomp.ssreflect.generic_quotient]
quo_mx_irr [in mathcomp.character.mxrepresentation]
quo_mx_quotient [in mathcomp.character.mxrepresentation]
quo_repr_coset [in mathcomp.character.mxrepresentation]
quo_mx_repr [in mathcomp.character.mxrepresentation]
quo_mx_coset [in mathcomp.character.mxrepresentation]
quo_IirrKeq [in mathcomp.character.character]
quo_IirrK [in mathcomp.character.character]
quo_Iirr_eq0 [in mathcomp.character.character]
quo_IirrE [in mathcomp.character.character]
quo_Iirr0 [in mathcomp.character.character]
Q8_extraspecial [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 (75489 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 (1813 entries)
Binder 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 (45320 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 (382 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 (3967 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 (91 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 (14046 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 (469 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 (128 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 (457 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 (1372 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 (1025 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 (6124 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 (250 entries)