Q (Definitions)
| 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 (Definitions)
qact [def, in mathcomp.finite_group.action]qact_dom [def, in mathcomp.finite_group.action]
qact_dom_group [def, in mathcomp.finite_group.action]
qfpoly [def, in mathcomp.field.qfpoly]
qfpoly_const [def, in mathcomp.field.qfpoly]
qfpoly_splitting_field_type [def, in mathcomp.field.qfpoly]
qidmx [def, in mathcomp.algebra.mxalgebra]
qisom [def, in mathcomp.finite_group.quotient]
qisom_morphism [def, in mathcomp.finite_group.quotient]
qlogp [def, in mathcomp.field.qfpoly]
qpoly [def, in mathcomp.algebra.qpoly]
qpoly1 [def, in mathcomp.algebra.qpoly]
qpoly_inv [def, in mathcomp.algebra.qpoly]
qpoly_mul [def, in mathcomp.algebra.qpoly]
qpoly_scale [def, in mathcomp.algebra.qpoly]
qpolyC [def, in mathcomp.algebra.qpoly]
qpolyC_is_additive [def, in mathcomp.algebra.qpoly]
qpolyC_is_multiplicative [def, in mathcomp.algebra.qpoly]
qpolyX [def, in mathcomp.algebra.qpoly]
Qrat [def, in mathcomp.algebra.binnums]
quaternion_gtype.body [def, in mathcomp.solvable.extremal]
quaternion_gtype.unlock [def, in mathcomp.solvable.extremal]
quaternion_gtype_unlock_subterm [def, in mathcomp.solvable.extremal]
quaternion_kernel [def, in mathcomp.solvable.extremal]
quaternion_unlock [def, in mathcomp.solvable.extremal]
quo_Iirr [def, in mathcomp.group_representation.character]
quo_mx [def, in mathcomp.group_representation.mxrepresentation]
quo_repr [def, in mathcomp.group_representation.mxrepresentation]
quot_pi_subdef [def, in mathcomp.boot.generic_quotient]
quot_type_of [def, in mathcomp.boot.generic_quotient]
quotient [def, in mathcomp.finite_group.quotient]
Quotient.add [def, in mathcomp.algebra.ring_quotient]
Quotient.equiv [def, in mathcomp.algebra.ring_quotient]
Quotient.equiv_encModRel [def, in mathcomp.algebra.ring_quotient]
Quotient.equiv_equiv [def, in mathcomp.algebra.ring_quotient]
Quotient.mul [def, in mathcomp.algebra.ring_quotient]
Quotient.one [def, in mathcomp.algebra.ring_quotient]
Quotient.opp [def, in mathcomp.algebra.ring_quotient]
Quotient.pack_ [def, in mathcomp.boot.generic_quotient]
Quotient.phant_clone [def, in mathcomp.boot.generic_quotient]
Quotient.phant_on_ [def, in mathcomp.boot.generic_quotient]
Quotient.pi_add_morph [def, in mathcomp.algebra.ring_quotient]
Quotient.pi_mul_morph [def, in mathcomp.algebra.ring_quotient]
Quotient.pi_one_morph [def, in mathcomp.algebra.ring_quotient]
Quotient.pi_opp_morph [def, in mathcomp.algebra.ring_quotient]
Quotient.pi_zero_morph [def, in mathcomp.algebra.ring_quotient]
Quotient.quot [def, in mathcomp.algebra.ring_quotient]
Quotient.zero [def, in mathcomp.algebra.ring_quotient]
quotient_action [def, in mathcomp.finite_group.action]
quotient_group [def, in mathcomp.finite_group.quotient]
quotient_groupAction [def, in mathcomp.finite_group.action]
quotient_of_section [def, in mathcomp.solvable.jordanholder]
quotm [def, in mathcomp.finite_group.quotient]
quotm_morphism [def, in mathcomp.finite_group.quotient]
QuotSubType.Sub [def, in mathcomp.boot.generic_quotient]