From ed05182cece6bb3706e09b2ce14af4a41a2e8141 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Apr 2018 10:54:22 +0200 Subject: generate the documentation for 1.7 --- docs/htmldoc/index_lemma_Q.html | 1091 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 1091 insertions(+) create mode 100644 docs/htmldoc/index_lemma_Q.html (limited to 'docs/htmldoc/index_lemma_Q.html') diff --git a/docs/htmldoc/index_lemma_Q.html b/docs/htmldoc/index_lemma_Q.html new file mode 100644 index 0000000..1b966ed --- /dev/null +++ b/docs/htmldoc/index_lemma_Q.html @@ -0,0 +1,1091 @@ + + + + + +mathcomp.ssreflect.tuple + + + + +
+ + + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(23233 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1373 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(213 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3475 entries)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(89 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(11853 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(359 entries)
Axiom IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(47 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(103 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(266 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1118 entries)
Abbreviation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(691 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3461 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(185 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_subring_closed [in mathcomp.algebra.rat]
+Qint_def [in mathcomp.algebra.rat]
+Qint_key [in mathcomp.algebra.rat]
+Qint_dvdz [in mathcomp.algebra.intdiv]
+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_semiring_closed [in mathcomp.algebra.rat]
+Qnat_def [in mathcomp.algebra.rat]
+Qnat_key [in mathcomp.algebra.rat]
+Qnat_dvd [in mathcomp.algebra.intdiv]
+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_TI_subcent [in mathcomp.solvable.hall]
+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_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_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_Phi [in mathcomp.solvable.maximal]
+quotient_astabQ [in mathcomp.fingroup.action]
+quotient_cfker_mod [in mathcomp.character.classfun]
+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_der [in mathcomp.solvable.commutator]
+quotient_cents2r [in mathcomp.solvable.commutator]
+quotient_cents2 [in mathcomp.solvable.commutator]
+quotient_generator [in mathcomp.solvable.cyclic]
+quotient_cyclic [in mathcomp.solvable.cyclic]
+quotient_cycle [in mathcomp.solvable.cyclic]
+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 IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(23233 entries)
Notation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1373 entries)
Module IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(213 entries)
Variable IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3475 entries)
Library IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(89 entries)
Lemma IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(11853 entries)
Constructor IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(359 entries)
Axiom IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(47 entries)
Inductive IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(103 entries)
Projection IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(266 entries)
Section IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(1118 entries)
Abbreviation IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(691 entries)
Definition IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(3461 entries)
Record IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_other(185 entries)
+
+ + + +
+ + + \ No newline at end of file -- cgit v1.2.3