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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |

## Q

q [definition, in extremal]q [definition, in extremal]

q [definition, in extremal]

q [definition, in extremal]

qact [definition, in action]

qactE [lemma, in action]

qactEcond [lemma, in action]

qactJ [lemma, in action]

qacts_coset [lemma, in jordanholder]

qacts_cosetpre [lemma, in jordanholder]

qact_dom_doms [lemma, in jordanholder]

qact_domE [lemma, in action]

qact_dom_group [definition, in action]

qact_is_groupAction [lemma, in action]

qact_proof [lemma, in action]

qact_dom [definition, in action]

qact_subdomE [lemma, in action]

QE [module, in ssralg]

qf_eval [abbreviation, in mxrepresentation]

qf_form [abbreviation, in mxrepresentation]

qidmx [definition, in mxalgebra]

qidmx_cap [definition, in mxalgebra]

qidmx_eq1 [definition, in mxalgebra]

qisom [definition, in quotient]

qisomE [lemma, in quotient]

qisom_isom [lemma, in quotient]

qisom_morphism [definition, in quotient]

qisom_ker_proof [lemma, in quotient]

qisom_isog [lemma, in quotient]

qisom_inj [lemma, in quotient]

qisom_restr_proof [lemma, in quotient]

Quantifiers [section, in fintype]

Quantifiers.T [variable, in fintype]

Quaternion [constructor, in extremal]

quaternion_gtype [definition, in extremal]

quaternion_kernel [definition, in extremal]

quaternion_structure [lemma, in extremal]

quaternion_classP [lemma, in extremal]

QuoMax [section, in gseries]

QuoMax.G [variable, in gseries]

QuoMax.gT [variable, in gseries]

QuoMax.H [variable, in gseries]

QuoMax.K [variable, in gseries]

quotient [definition, in quotient]

quotient [library]

QuotientAbelem [section, in abelian]

QuotientAbelem.gT [variable, in abelian]

QuotientAbelem.p [variable, in abelian]

QuotientAction [section, in action]

QuotientAction.aT [variable, in action]

QuotientAction.D [variable, in action]

QuotientAction.H [variable, in action]

QuotientAction.rT [variable, in action]

QuotientAction.to [variable, in action]

quotientD [lemma, in quotient]

quotientDG [lemma, in quotient]

quotientE [lemma, in quotient]

quotientGI [lemma, in quotient]

quotientGK [lemma, in quotient]

quotientI [lemma, in quotient]

quotientIG [lemma, in quotient]

quotientInorm [lemma, in quotient]

QuotientInternalProd [section, in gproduct]

QuotientInternalProd.G [variable, in gproduct]

QuotientInternalProd.gT [variable, in gproduct]

QuotientInternalProd.H [variable, in gproduct]

QuotientInternalProd.K [variable, in gproduct]

QuotientInternalProd.M [variable, in gproduct]

QuotientInternalProd.nMG [variable, in gproduct]

quotientJ [lemma, in quotient]

quotientK [lemma, in quotient]

quotientMidl [lemma, in quotient]

quotientMidr [lemma, in quotient]

quotientMl [lemma, in quotient]

QuotientMorphism [section, in quotient]

QuotientMorphism.f [variable, in quotient]

QuotientMorphism.G [variable, in quotient]

QuotientMorphism.gT [variable, in quotient]

QuotientMorphism.H [variable, in quotient]

QuotientMorphism.nsHG [variable, in quotient]

QuotientMorphism.rT [variable, in quotient]

quotientMr [lemma, in quotient]

QuotientNil [section, in nilpotent]

QuotientNil.gT [variable, in nilpotent]

quotientR [lemma, in quotient]

QuotientRank [section, in abelian]

QuotientRank.cGG [variable, in abelian]

QuotientRank.G [variable, in abelian]

QuotientRank.gT [variable, in abelian]

QuotientRank.H [variable, in abelian]

QuotientRank.p [variable, in abelian]

quotientS [lemma, in quotient]

quotientSGK [lemma, in quotient]

quotientSK [lemma, in quotient]

QuotientSol [section, in nilpotent]

QuotientSol.gT [variable, in nilpotent]

QuotientSol.rT [variable, in nilpotent]

quotientS1 [lemma, in quotient]

quotientT [lemma, in quotient]

quotientU [lemma, in quotient]

quotientV [lemma, in quotient]

quotientY [lemma, in quotient]

quotientYidl [lemma, in quotient]

quotientYidr [lemma, in quotient]

quotientYK [lemma, in quotient]

quotient_cent [lemma, in quotient]

quotient_abelian [lemma, in quotient]

quotient_subcent [lemma, in quotient]

quotient_coprime_dprod [lemma, in gproduct]

quotient_abelem [lemma, in abelian]

quotient_Ldiv [lemma, in abelian]

quotient_of_section [definition, in jordanholder]

quotient_proper [lemma, in quotient]

quotient_isog [lemma, in quotient]

quotient_cprod [lemma, in gproduct]

quotient_group [definition, in quotient]

quotient_cent1s [lemma, in quotient]

quotient_cycle [lemma, in cyclic]

quotient_cent1 [lemma, in quotient]

quotient_center_nil [lemma, in nilpotent]

quotient_cents [lemma, in quotient]

quotient_LdivT [lemma, in abelian]

quotient_nil [lemma, in nilpotent]

quotient_subnorm [lemma, in quotient]

quotient_injG [lemma, in quotient]

quotient_coprime_sdprod [lemma, in gproduct]

quotient_pseries2 [lemma, in pgroup]

quotient_odd [lemma, in pgroup]

quotient_rank_abelian [lemma, in abelian]

quotient_TI_subcent [lemma, in hall]

quotient_cents2r [lemma, in commutator]

quotient_normG [lemma, in quotient]

quotient_simple [lemma, in gseries]

quotient_isom [lemma, in quotient]

quotient_ucn_add [lemma, in nilpotent]

quotient_homg [lemma, in quotient]

quotient_cyclic [lemma, in cyclic]

quotient_norm [lemma, in quotient]

quotient_normal [lemma, in quotient]

quotient_pElem [lemma, in abelian]

quotient_sub1 [lemma, in quotient]

quotient_inj [lemma, in quotient]

quotient_subnormG [lemma, in quotient]

quotient_norms [lemma, in quotient]

quotient_gen [lemma, in quotient]

quotient_cents2 [lemma, in commutator]

quotient_pcore_mod [lemma, in pgroup]

quotient_p_rank_abelian [lemma, in abelian]

quotient_sol [lemma, in nilpotent]

quotient_groupAction [definition, in action]

quotient_action [definition, in action]

quotient_astabQ [lemma, in action]

quotient_subnormal [lemma, in gseries]

quotient_maximal [lemma, in gseries]

quotient_pseries [lemma, in pgroup]

quotient_subcent1 [lemma, in quotient]

quotient_Phi [lemma, in maximal]

quotient_der [lemma, in commutator]

quotient_pseries_cat [lemma, in pgroup]

quotient_splitting_field [lemma, in mxrepresentation]

quotient_generator [lemma, in cyclic]

quotient_pgroup [lemma, in pgroup]

quotient_maximal_eq [lemma, in gseries]

quotient_pprod [lemma, in gproduct]

quotient_pHall [lemma, in pgroup]

quotient_set1 [lemma, in quotient]

quotient_grank [lemma, in abelian]

quotient0 [lemma, in quotient]

Quotient1 [section, in quotient]

quotient1 [lemma, in quotient]

quotient1_isom [lemma, in quotient]

quotient1_isog [lemma, in quotient]

Quotient1.A [variable, in quotient]

Quotient1.gT [variable, in quotient]

quotm [definition, in quotient]

quotmE [lemma, in quotient]

quotm_dom_proof [lemma, in quotient]

quotm_morphism [definition, in quotient]

quotm_ker_proof [lemma, in quotient]

quo_repr_coset [lemma, in mxrepresentation]

quo_mx_repr [lemma, in mxrepresentation]

quo_repr [definition, in mxrepresentation]

quo_mx_irr [lemma, in mxrepresentation]

quo_mx_coset [lemma, in mxrepresentation]

quo_mx [definition, in mxrepresentation]

quo_mx_quotient [lemma, in mxrepresentation]

q_gt0 [definition, in extremal]

q_gt1 [definition, in extremal]

Q8_extraspecial [lemma, in 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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |