Q (Lemmas)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
Q (Lemmas)
Q8_extraspecial [prf, in mathcomp.solvable.extraspecial]qact_dom_doms [prf, in mathcomp.solvable.jordanholder]
qact_domE [prf, in mathcomp.finite_group.action]
qact_is_groupAction [prf, in mathcomp.finite_group.action]
qact_proof [prf, in mathcomp.finite_group.action]
qact_subdomE [prf, in mathcomp.finite_group.action]
qactE [prf, in mathcomp.finite_group.action]
qactEcond [prf, in mathcomp.finite_group.action]
qactJ [prf, in mathcomp.finite_group.action]
qacts_coset [prf, in mathcomp.solvable.jordanholder]
qacts_cosetpre [prf, in mathcomp.solvable.jordanholder]
Qint_def [prf, in mathcomp.algebra.rat]
Qint_dvdz [prf, in mathcomp.algebra.rat]
qisom_inj [prf, in mathcomp.finite_group.quotient]
qisom_isog [prf, in mathcomp.finite_group.quotient]
qisom_isom [prf, in mathcomp.finite_group.quotient]
qisom_ker_proof [prf, in mathcomp.finite_group.quotient]
qisom_restr_proof [prf, in mathcomp.finite_group.quotient]
qisomE [prf, in mathcomp.finite_group.quotient]
qlogp0 [prf, in mathcomp.field.qfpoly]
qlogp1 [prf, in mathcomp.field.qfpoly]
qlogp_eq0 [prf, in mathcomp.field.qfpoly]
qlogp_lt [prf, in mathcomp.field.qfpoly]
qlogp_qX [prf, in mathcomp.field.qfpoly]
qlogpD [prf, in mathcomp.field.qfpoly]
Qn_aut_exists [prf, in mathcomp.field.algnum]
Qnat_dvd [prf, in mathcomp.algebra.rat]
qpoly_intro_unit [prf, in mathcomp.algebra.qpoly]
qpoly_inv0 [prf, in mathcomp.field.qfpoly]
qpoly_inv_out [prf, in mathcomp.algebra.qpoly]
qpoly_mul1z [prf, in mathcomp.algebra.qpoly]
qpoly_mul_addl [prf, in mathcomp.algebra.qpoly]
qpoly_mul_addr [prf, in mathcomp.algebra.qpoly]
qpoly_mulA [prf, in mathcomp.algebra.qpoly]
qpoly_mulC [prf, in mathcomp.algebra.qpoly]
qpoly_mulVp [prf, in mathcomp.field.qfpoly]
qpoly_mulVz [prf, in mathcomp.algebra.qpoly]
qpoly_mulz1 [prf, in mathcomp.algebra.qpoly]
qpoly_mulzV [prf, in mathcomp.algebra.qpoly]
qpoly_nontrivial [prf, in mathcomp.algebra.qpoly]
qpoly_scale1l [prf, in mathcomp.algebra.qpoly]
qpoly_scaleA [prf, in mathcomp.algebra.qpoly]
qpoly_scaleAl [prf, in mathcomp.algebra.qpoly]
qpoly_scaleAr [prf, in mathcomp.algebra.qpoly]
qpoly_scaleDl [prf, in mathcomp.algebra.qpoly]
qpoly_scaleDr [prf, in mathcomp.algebra.qpoly]
qpolyC0 [prf, in mathcomp.algebra.qpoly]
qpolyC_is_monoid_morphism [prf, in mathcomp.algebra.qpoly]
qpolyC_is_zmod_morphism [prf, in mathcomp.algebra.qpoly]
qpolyC_natr [prf, in mathcomp.algebra.qpoly]
qpolyC_proof [prf, in mathcomp.algebra.qpoly]
qpolyCD [prf, in mathcomp.algebra.qpoly]
qpolyCE [prf, in mathcomp.algebra.qpoly]
qpolyCM [prf, in mathcomp.algebra.qpoly]
qpolyCN [prf, in mathcomp.algebra.qpoly]
qpolyXE [prf, in mathcomp.algebra.qpoly]
Qrat0 [prf, in mathcomp.algebra.binnums]
Qrat1 [prf, in mathcomp.algebra.binnums]
Qrat_eq [prf, in mathcomp.algebra.binnums]
Qrat_le [prf, in mathcomp.algebra.binnums]
Qrat_Qmake [prf, in mathcomp.algebra.binnums]
Qrat_rat_of_Q [prf, in mathcomp.algebra.binnums]
Qrat_spec_Q_to_rat [prf, in mathcomp.algebra.binnums]
QratB [prf, in mathcomp.algebra.binnums]
QratD [prf, in mathcomp.algebra.binnums]
QratM [prf, in mathcomp.algebra.binnums]
QratN [prf, in mathcomp.algebra.binnums]
QratP [prf, in mathcomp.algebra.binnums]
QratV [prf, in mathcomp.algebra.binnums]
quaternion_classP [prf, in mathcomp.solvable.extremal]
quaternion_structure [prf, in mathcomp.solvable.extremal]
quo_Iirr0 [prf, in mathcomp.group_representation.character]
quo_Iirr_eq0 [prf, in mathcomp.group_representation.character]
quo_IirrE [prf, in mathcomp.group_representation.character]
quo_IirrK [prf, in mathcomp.group_representation.character]
quo_IirrKeq [prf, in mathcomp.group_representation.character]
quo_mx_coset [prf, in mathcomp.group_representation.mxrepresentation]
quo_mx_irr [prf, in mathcomp.group_representation.mxrepresentation]
quo_mx_quotient [prf, in mathcomp.group_representation.mxrepresentation]
quo_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
quo_repr_coset [prf, in mathcomp.group_representation.mxrepresentation]
Quotient.add0q [prf, in mathcomp.algebra.ring_quotient]
Quotient.addNq [prf, in mathcomp.algebra.ring_quotient]
Quotient.addqA [prf, in mathcomp.algebra.ring_quotient]
Quotient.addqC [prf, in mathcomp.algebra.ring_quotient]
Quotient.equiv_is_equiv [prf, in mathcomp.algebra.ring_quotient]
Quotient.equivE [prf, in mathcomp.algebra.ring_quotient]
Quotient.idealrBE [prf, in mathcomp.algebra.ring_quotient]
Quotient.idealrDE [prf, in mathcomp.algebra.ring_quotient]
Quotient.mul1q [prf, in mathcomp.algebra.ring_quotient]
Quotient.mulq_addl [prf, in mathcomp.algebra.ring_quotient]
Quotient.mulqA [prf, in mathcomp.algebra.ring_quotient]
Quotient.mulqC [prf, in mathcomp.algebra.ring_quotient]
Quotient.nonzero1q [prf, in mathcomp.algebra.ring_quotient]
Quotient.pi_add [prf, in mathcomp.algebra.ring_quotient]
Quotient.pi_mul [prf, in mathcomp.algebra.ring_quotient]
Quotient.pi_opp [prf, in mathcomp.algebra.ring_quotient]
Quotient.rquot_IdomainAxiom [prf, in mathcomp.algebra.ring_quotient]
quotient0 [prf, in mathcomp.finite_group.quotient]
quotient1 [prf, in mathcomp.finite_group.quotient]
quotient1_isog [prf, in mathcomp.finite_group.quotient]
quotient1_isom [prf, in mathcomp.finite_group.quotient]
quotient_abelem [prf, in mathcomp.solvable.abelian]
quotient_abelian [prf, in mathcomp.finite_group.quotient]
quotient_astabQ [prf, in mathcomp.finite_group.action]
quotient_cent [prf, in mathcomp.finite_group.quotient]
quotient_cent1 [prf, in mathcomp.finite_group.quotient]
quotient_cent1s [prf, in mathcomp.finite_group.quotient]
quotient_center_nil [prf, in mathcomp.solvable.nilpotent]
quotient_cents [prf, in mathcomp.finite_group.quotient]
quotient_cents2 [prf, in mathcomp.solvable.commutator]
quotient_cents2r [prf, in mathcomp.solvable.commutator]
quotient_cfker_mod [prf, in mathcomp.group_representation.classfun]
quotient_class [prf, in mathcomp.finite_group.quotient]
quotient_coprime_dprod [prf, in mathcomp.finite_group.gproduct]
quotient_coprime_sdprod [prf, in mathcomp.finite_group.gproduct]
quotient_cprod [prf, in mathcomp.finite_group.gproduct]
quotient_cycle [prf, in mathcomp.solvable.cyclic]
quotient_cyclic [prf, in mathcomp.solvable.cyclic]
quotient_der [prf, in mathcomp.solvable.commutator]
quotient_gen [prf, in mathcomp.finite_group.quotient]
quotient_generator [prf, in mathcomp.solvable.cyclic]
quotient_grank [prf, in mathcomp.solvable.abelian]
quotient_homg [prf, in mathcomp.finite_group.quotient]
quotient_inj [prf, in mathcomp.finite_group.quotient]
quotient_injG [prf, in mathcomp.finite_group.quotient]
quotient_isog [prf, in mathcomp.finite_group.quotient]
quotient_isom [prf, in mathcomp.finite_group.quotient]
quotient_Ldiv [prf, in mathcomp.solvable.abelian]
quotient_LdivT [prf, in mathcomp.solvable.abelian]
quotient_maximal [prf, in mathcomp.solvable.gseries]
quotient_maximal_eq [prf, in mathcomp.solvable.gseries]
quotient_neq1 [prf, in mathcomp.finite_group.quotient]
quotient_nil [prf, in mathcomp.solvable.nilpotent]
quotient_norm [prf, in mathcomp.finite_group.quotient]
quotient_normal [prf, in mathcomp.finite_group.quotient]
quotient_normG [prf, in mathcomp.finite_group.quotient]
quotient_norms [prf, in mathcomp.finite_group.quotient]
quotient_odd [prf, in mathcomp.solvable.pgroup]
quotient_p_rank_abelian [prf, in mathcomp.solvable.abelian]
quotient_pcore_mod [prf, in mathcomp.solvable.pgroup]
quotient_pElem [prf, in mathcomp.solvable.abelian]
quotient_pgroup [prf, in mathcomp.solvable.pgroup]
quotient_pHall [prf, in mathcomp.solvable.pgroup]
quotient_Phi [prf, in mathcomp.solvable.maximal]
quotient_pnElem [prf, in mathcomp.solvable.abelian]
quotient_pprod [prf, in mathcomp.finite_group.gproduct]
quotient_proper [prf, in mathcomp.finite_group.quotient]
quotient_pseries [prf, in mathcomp.solvable.pgroup]
quotient_pseries2 [prf, in mathcomp.solvable.pgroup]
quotient_pseries_cat [prf, in mathcomp.solvable.pgroup]
quotient_rank_abelian [prf, in mathcomp.solvable.abelian]
quotient_sdprodr_isog [prf, in mathcomp.finite_group.gproduct]
quotient_sdprodr_isom [prf, in mathcomp.finite_group.gproduct]
quotient_set1 [prf, in mathcomp.finite_group.quotient]
quotient_setIpre [prf, in mathcomp.finite_group.quotient]
quotient_simple [prf, in mathcomp.solvable.gseries]
quotient_sol [prf, in mathcomp.solvable.nilpotent]
quotient_splitting_field [prf, in mathcomp.group_representation.mxrepresentation]
quotient_sub1 [prf, in mathcomp.finite_group.quotient]
quotient_subcent [prf, in mathcomp.finite_group.quotient]
quotient_subcent1 [prf, in mathcomp.finite_group.quotient]
quotient_subnorm [prf, in mathcomp.finite_group.quotient]
quotient_subnormal [prf, in mathcomp.solvable.gseries]
quotient_subnormG [prf, in mathcomp.finite_group.quotient]
quotient_TI_subcent [prf, in mathcomp.solvable.hall]
quotient_ucn_add [prf, in mathcomp.solvable.nilpotent]
quotientD [prf, in mathcomp.finite_group.quotient]
quotientD1 [prf, in mathcomp.finite_group.quotient]
quotientDG [prf, in mathcomp.finite_group.quotient]
quotientE [prf, in mathcomp.finite_group.quotient]
quotientGI [prf, in mathcomp.finite_group.quotient]
quotientGK [prf, in mathcomp.finite_group.quotient]
quotientI [prf, in mathcomp.finite_group.quotient]
quotientIG [prf, in mathcomp.finite_group.quotient]
quotientInorm [prf, in mathcomp.finite_group.quotient]
quotientJ [prf, in mathcomp.finite_group.quotient]
quotientK [prf, in mathcomp.finite_group.quotient]
quotientMidl [prf, in mathcomp.finite_group.quotient]
quotientMidr [prf, in mathcomp.finite_group.quotient]
quotientMl [prf, in mathcomp.finite_group.quotient]
quotientMr [prf, in mathcomp.finite_group.quotient]
quotientR [prf, in mathcomp.finite_group.quotient]
quotientS [prf, in mathcomp.finite_group.quotient]
quotientS1 [prf, in mathcomp.finite_group.quotient]
quotientSGK [prf, in mathcomp.finite_group.quotient]
quotientSK [prf, in mathcomp.finite_group.quotient]
quotientT [prf, in mathcomp.finite_group.quotient]
quotientU [prf, in mathcomp.finite_group.quotient]
quotientV [prf, in mathcomp.finite_group.quotient]
quotientY [prf, in mathcomp.finite_group.quotient]
quotientYidl [prf, in mathcomp.finite_group.quotient]
quotientYidr [prf, in mathcomp.finite_group.quotient]
quotientYK [prf, in mathcomp.finite_group.quotient]
quotm_dom_proof [prf, in mathcomp.finite_group.quotient]
quotm_ker_proof [prf, in mathcomp.finite_group.quotient]
quotmE [prf, in mathcomp.finite_group.quotient]
quotP [prf, in mathcomp.boot.generic_quotient]
QuotSubType.qreprK [prf, in mathcomp.boot.generic_quotient]
QuotSubType.reprP [prf, in mathcomp.boot.generic_quotient]
QuotSubType.sort_Sub [prf, in mathcomp.boot.generic_quotient]
QuotSubType.sortPx [prf, in mathcomp.boot.generic_quotient]
quotW [prf, in mathcomp.boot.generic_quotient]
qX_exp_inj [prf, in mathcomp.field.qfpoly]
qX_exp_neq0 [prf, in mathcomp.field.qfpoly]
qX_expK [prf, in mathcomp.field.qfpoly]
qX_in_unit [prf, in mathcomp.field.qfpoly]
qX_neq0 [prf, in mathcomp.field.qfpoly]
qX_order_card [prf, in mathcomp.field.qfpoly]
qX_order_dvd [prf, in mathcomp.field.qfpoly]