| 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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +
M
+mact [definition, in mathcomp.fingroup.action]+mactE [lemma, in mathcomp.fingroup.action]
+mact_is_action [lemma, in mathcomp.fingroup.action]
+MakeAut [section, in mathcomp.fingroup.automorphism]
+MakeAut.f [variable, in mathcomp.fingroup.automorphism]
+MakeAut.G [variable, in mathcomp.fingroup.automorphism]
+MakeAut.Gf [variable, in mathcomp.fingroup.automorphism]
+MakeAut.gT [variable, in mathcomp.fingroup.automorphism]
+MakeAut.injf [variable, in mathcomp.fingroup.automorphism]
+MakeEqSeq [section, in mathcomp.ssreflect.seq]
+MakeEqSeq.T [variable, in mathcomp.ssreflect.seq]
+MakeEqTypePred [module, in mathcomp.ssreflect.eqtype]
+MakeGroupSetBaseGroup [module, in mathcomp.fingroup.fingroup]
+MakeSeq [section, in mathcomp.ssreflect.seq]
+MakeSeq.T [variable, in mathcomp.ssreflect.seq]
+MakeSeq.x0 [variable, in mathcomp.ssreflect.seq]
+make_separable [lemma, in mathcomp.field.separable]
+map [definition, in mathcomp.ssreflect.seq]
+Map [section, in mathcomp.ssreflect.seq]
+MapComp [section, in mathcomp.ssreflect.seq]
+MapComp.T1 [variable, in mathcomp.ssreflect.seq]
+MapComp.T2 [variable, in mathcomp.ssreflect.seq]
+MapComp.T3 [variable, in mathcomp.ssreflect.seq]
+MapComRing [section, in mathcomp.algebra.mxpoly]
+MapComRing.A [variable, in mathcomp.algebra.mxpoly]
+MapComRing.aR [variable, in mathcomp.algebra.mxpoly]
+MapComRing.f [variable, in mathcomp.algebra.mxpoly]
+MapComRing.n' [variable, in mathcomp.algebra.mxpoly]
+MapComRing.rR [variable, in mathcomp.algebra.mxpoly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.mxpoly]
+MapEqPath [section, in mathcomp.ssreflect.path]
+MapEqPath.e [variable, in mathcomp.ssreflect.path]
+MapEqPath.e' [variable, in mathcomp.ssreflect.path]
+MapEqPath.h [variable, in mathcomp.ssreflect.path]
+MapEqPath.Ih [variable, in mathcomp.ssreflect.path]
+MapEqPath.T [variable, in mathcomp.ssreflect.path]
+MapEqPath.T' [variable, in mathcomp.ssreflect.path]
+MapField [section, in mathcomp.algebra.mxpoly]
+MapFieldMatrix [section, in mathcomp.algebra.matrix]
+MapFieldMatrix.aF [variable, in mathcomp.algebra.matrix]
+MapFieldMatrix.f [variable, in mathcomp.algebra.matrix]
+MapFieldMatrix.rF [variable, in mathcomp.algebra.matrix]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
+MapFieldPoly [section, in mathcomp.algebra.poly]
+MapFieldPoly.f [variable, in mathcomp.algebra.poly]
+MapFieldPoly.F [variable, in mathcomp.algebra.poly]
+MapFieldPoly.R [variable, in mathcomp.algebra.poly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
+MapField.A [variable, in mathcomp.algebra.mxpoly]
+MapField.aF [variable, in mathcomp.algebra.mxpoly]
+MapField.f [variable, in mathcomp.algebra.mxpoly]
+MapField.n' [variable, in mathcomp.algebra.mxpoly]
+MapField.rF [variable, in mathcomp.algebra.mxpoly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.mxpoly]
+mapK [lemma, in mathcomp.ssreflect.seq]
+MapMatrix [section, in mathcomp.algebra.matrix]
+MapMatrixSpaces [section, in mathcomp.algebra.mxalgebra]
+MapMatrixSpaces.aF [variable, in mathcomp.algebra.mxalgebra]
+MapMatrixSpaces.f [variable, in mathcomp.algebra.mxalgebra]
+MapMatrixSpaces.rF [variable, in mathcomp.algebra.mxalgebra]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.mxalgebra]
+MapMatrix.aT [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block [section, in mathcomp.algebra.matrix]
+MapMatrix.Block.Adl [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.Adr [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.Aul [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.Aur [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.B [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.Bh [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.Bv [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.m1 [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.m2 [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.n1 [variable, in mathcomp.algebra.matrix]
+MapMatrix.Block.n2 [variable, in mathcomp.algebra.matrix]
+MapMatrix.f [variable, in mathcomp.algebra.matrix]
+MapMatrix.OneMatrix [section, in mathcomp.algebra.matrix]
+MapMatrix.OneMatrix.A [variable, in mathcomp.algebra.matrix]
+MapMatrix.OneMatrix.m [variable, in mathcomp.algebra.matrix]
+MapMatrix.OneMatrix.n [variable, in mathcomp.algebra.matrix]
+MapMatrix.rT [variable, in mathcomp.algebra.matrix]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
+MapMinPoly [section, in mathcomp.field.fieldext]
+MapMinPoly.f [variable, in mathcomp.field.fieldext]
+MapMinPoly.F0 [variable, in mathcomp.field.fieldext]
+MapMinPoly.K [variable, in mathcomp.field.fieldext]
+MapMinPoly.L [variable, in mathcomp.field.fieldext]
+MapMinPoly.rL [variable, in mathcomp.field.fieldext]
+MapMinPoly.x [variable, in mathcomp.field.fieldext]
+mapP [lemma, in mathcomp.ssreflect.seq]
+MapPath [section, in mathcomp.ssreflect.path]
+MapPath.e [variable, in mathcomp.ssreflect.path]
+MapPath.e' [variable, in mathcomp.ssreflect.path]
+MapPath.h [variable, in mathcomp.ssreflect.path]
+MapPath.T [variable, in mathcomp.ssreflect.path]
+MapPath.T' [variable, in mathcomp.ssreflect.path]
+MapPoly [section, in mathcomp.algebra.poly]
+MapPolyRoots [section, in mathcomp.algebra.poly]
+MapPolyRoots.f [variable, in mathcomp.algebra.poly]
+MapPolyRoots.F [variable, in mathcomp.algebra.poly]
+MapPolyRoots.R [variable, in mathcomp.algebra.poly]
+MapPoly.Additive [section, in mathcomp.algebra.poly]
+MapPoly.Additive.f [variable, in mathcomp.algebra.poly]
+MapPoly.Additive.iR [variable, in mathcomp.algebra.poly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
+MapPoly.aR [variable, in mathcomp.algebra.poly]
+MapPoly.Combinatorial [section, in mathcomp.algebra.poly]
+MapPoly.Combinatorial.f [variable, in mathcomp.algebra.poly]
+MapPoly.Combinatorial.f_0 [variable, in mathcomp.algebra.poly]
+MapPoly.Combinatorial.inj_f [variable, in mathcomp.algebra.poly]
+MapPoly.Combinatorial.iR [variable, in mathcomp.algebra.poly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
+MapPoly.Definitions [section, in mathcomp.algebra.poly]
+MapPoly.Definitions.aR [variable, in mathcomp.algebra.poly]
+MapPoly.Definitions.f [variable, in mathcomp.algebra.poly]
+MapPoly.Definitions.rR [variable, in mathcomp.algebra.poly]
+MapPoly.f [variable, in mathcomp.algebra.poly]
+MapPoly.HornerMorph [section, in mathcomp.algebra.poly]
+MapPoly.HornerMorph.cfu [variable, in mathcomp.algebra.poly]
+MapPoly.HornerMorph.u [variable, in mathcomp.algebra.poly]
+MapPoly.rR [variable, in mathcomp.algebra.poly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.poly]
+MapResultant [section, in mathcomp.algebra.mxpoly]
+MapRingMatrix [section, in mathcomp.algebra.matrix]
+MapRingMatrix [section, in mathcomp.algebra.mxpoly]
+MapRingMatrix.A [variable, in mathcomp.algebra.mxpoly]
+MapRingMatrix.aR [variable, in mathcomp.algebra.matrix]
+MapRingMatrix.aR [variable, in mathcomp.algebra.mxpoly]
+MapRingMatrix.d [variable, in mathcomp.algebra.mxpoly]
+MapRingMatrix.f [variable, in mathcomp.algebra.matrix]
+MapRingMatrix.f [variable, in mathcomp.algebra.mxpoly]
+MapRingMatrix.FixedSize [section, in mathcomp.algebra.matrix]
+MapRingMatrix.FixedSize.m [variable, in mathcomp.algebra.matrix]
+MapRingMatrix.FixedSize.n [variable, in mathcomp.algebra.matrix]
+MapRingMatrix.FixedSize.p [variable, in mathcomp.algebra.matrix]
+MapRingMatrix.n [variable, in mathcomp.algebra.mxpoly]
+MapRingMatrix.rR [variable, in mathcomp.algebra.matrix]
+MapRingMatrix.rR [variable, in mathcomp.algebra.mxpoly]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.mxpoly]
+MapZmodMatrix [section, in mathcomp.algebra.matrix]
+MapZmodMatrix.aR [variable, in mathcomp.algebra.matrix]
+MapZmodMatrix.f [variable, in mathcomp.algebra.matrix]
+MapZmodMatrix.m [variable, in mathcomp.algebra.matrix]
+MapZmodMatrix.n [variable, in mathcomp.algebra.matrix]
+MapZmodMatrix.rR [variable, in mathcomp.algebra.matrix]
+_ ^f (ring_scope) [notation, in mathcomp.algebra.matrix]
+map_path [lemma, in mathcomp.ssreflect.path]
+map_orthonormal [lemma, in mathcomp.character.vcharacter]
+map_pairwise_orthogonal [lemma, in mathcomp.character.vcharacter]
+map_minPoly [lemma, in mathcomp.field.fieldext]
+map_regular_subseries [lemma, in mathcomp.character.mxrepresentation]
+map_section_repr [lemma, in mathcomp.character.mxrepresentation]
+map_mx_abs_irr [lemma, in mathcomp.character.mxrepresentation]
+map_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
+map_rfix_mx [lemma, in mathcomp.character.mxrepresentation]
+map_group_ring [lemma, in mathcomp.character.mxrepresentation]
+map_regular_repr [lemma, in mathcomp.character.mxrepresentation]
+map_gring_op [lemma, in mathcomp.character.mxrepresentation]
+map_gring_mx [lemma, in mathcomp.character.mxrepresentation]
+map_enveloping_algebra_mx [lemma, in mathcomp.character.mxrepresentation]
+map_reprJ [lemma, in mathcomp.character.mxrepresentation]
+map_reprE [lemma, in mathcomp.character.mxrepresentation]
+map_mx_repr [lemma, in mathcomp.character.mxrepresentation]
+map_repr_mx [definition, in mathcomp.character.mxrepresentation]
+map_gring_proj [lemma, in mathcomp.character.mxrepresentation]
+map_gring_row [lemma, in mathcomp.character.mxrepresentation]
+map_regular_mx [lemma, in mathcomp.character.mxrepresentation]
+map_poly_divzK [lemma, in mathcomp.algebra.intdiv]
+map_tupleP [lemma, in mathcomp.ssreflect.tuple]
+map_tnth_enum [lemma, in mathcomp.ssreflect.tuple]
+map_mx_eq0 [lemma, in mathcomp.algebra.matrix]
+map_mx_inv [lemma, in mathcomp.algebra.matrix]
+map_invmx [lemma, in mathcomp.algebra.matrix]
+map_mx_unit [lemma, in mathcomp.algebra.matrix]
+map_unitmx [lemma, in mathcomp.algebra.matrix]
+map_mx_is_scalar [lemma, in mathcomp.algebra.matrix]
+map_mx_inj [lemma, in mathcomp.algebra.matrix]
+map_lin_mx [lemma, in mathcomp.algebra.matrix]
+map_lin1_mx [lemma, in mathcomp.algebra.matrix]
+map_mx_is_multiplicative [lemma, in mathcomp.algebra.matrix]
+map_copid_mx [lemma, in mathcomp.algebra.matrix]
+map_mx_adj [lemma, in mathcomp.algebra.matrix]
+map_pid_mx [lemma, in mathcomp.algebra.matrix]
+map_tperm_mx [lemma, in mathcomp.algebra.matrix]
+map_perm_mx [lemma, in mathcomp.algebra.matrix]
+map_mx1 [lemma, in mathcomp.algebra.matrix]
+map_scalar_mx [lemma, in mathcomp.algebra.matrix]
+map_diag_mx [lemma, in mathcomp.algebra.matrix]
+map_delta_mx [lemma, in mathcomp.algebra.matrix]
+map_mxM [lemma, in mathcomp.algebra.matrix]
+map_mxZ [lemma, in mathcomp.algebra.matrix]
+map_mx_sum [definition, in mathcomp.algebra.matrix]
+map_mx_sub [lemma, in mathcomp.algebra.matrix]
+map_mxD [lemma, in mathcomp.algebra.matrix]
+map_mxN [lemma, in mathcomp.algebra.matrix]
+map_mx0 [lemma, in mathcomp.algebra.matrix]
+map_drsubmx [lemma, in mathcomp.algebra.matrix]
+map_dlsubmx [lemma, in mathcomp.algebra.matrix]
+map_ursubmx [lemma, in mathcomp.algebra.matrix]
+map_ulsubmx [lemma, in mathcomp.algebra.matrix]
+map_dsubmx [lemma, in mathcomp.algebra.matrix]
+map_usubmx [lemma, in mathcomp.algebra.matrix]
+map_rsubmx [lemma, in mathcomp.algebra.matrix]
+map_lsubmx [lemma, in mathcomp.algebra.matrix]
+map_block_mx [lemma, in mathcomp.algebra.matrix]
+map_col_mx [lemma, in mathcomp.algebra.matrix]
+map_row_mx [lemma, in mathcomp.algebra.matrix]
+map_vec_mx [lemma, in mathcomp.algebra.matrix]
+map_mxvec [lemma, in mathcomp.algebra.matrix]
+map_conform_mx [lemma, in mathcomp.algebra.matrix]
+map_castmx [lemma, in mathcomp.algebra.matrix]
+map_xcol [lemma, in mathcomp.algebra.matrix]
+map_xrow [lemma, in mathcomp.algebra.matrix]
+map_col_perm [lemma, in mathcomp.algebra.matrix]
+map_row_perm [lemma, in mathcomp.algebra.matrix]
+map_col' [lemma, in mathcomp.algebra.matrix]
+map_row' [lemma, in mathcomp.algebra.matrix]
+map_col [lemma, in mathcomp.algebra.matrix]
+map_row [lemma, in mathcomp.algebra.matrix]
+map_const_mx [lemma, in mathcomp.algebra.matrix]
+map_trmx [lemma, in mathcomp.algebra.matrix]
+map_mx [definition, in mathcomp.algebra.matrix]
+map_mx_key [lemma, in mathcomp.algebra.matrix]
+map_mx_inv_horner [lemma, in mathcomp.algebra.mxpoly]
+map_horner_mx [lemma, in mathcomp.algebra.mxpoly]
+map_powers_mx [lemma, in mathcomp.algebra.mxpoly]
+map_resultant [lemma, in mathcomp.algebra.mxpoly]
+map_char_poly [lemma, in mathcomp.algebra.mxpoly]
+map_char_poly_mx [lemma, in mathcomp.algebra.mxpoly]
+map_poly_rV [lemma, in mathcomp.algebra.mxpoly]
+map_rVpoly [lemma, in mathcomp.algebra.mxpoly]
+map_div_annihilantP [lemma, in mathcomp.algebra.polyXY]
+map_sub_annihilantP [lemma, in mathcomp.algebra.polyXY]
+map_Qnum_poly [lemma, in mathcomp.field.algnum]
+map_reshape [lemma, in mathcomp.ssreflect.seq]
+map_flatten [lemma, in mathcomp.ssreflect.seq]
+map_pK [lemma, in mathcomp.ssreflect.seq]
+map_id_in [lemma, in mathcomp.ssreflect.seq]
+map_comp [lemma, in mathcomp.ssreflect.seq]
+map_id [lemma, in mathcomp.ssreflect.seq]
+map_of_seq [lemma, in mathcomp.ssreflect.seq]
+map_inj_uniq [lemma, in mathcomp.ssreflect.seq]
+map_subseq [lemma, in mathcomp.ssreflect.seq]
+map_inj_in_uniq [lemma, in mathcomp.ssreflect.seq]
+map_uniq [lemma, in mathcomp.ssreflect.seq]
+map_f [lemma, in mathcomp.ssreflect.seq]
+map_mask [lemma, in mathcomp.ssreflect.seq]
+map_rev [lemma, in mathcomp.ssreflect.seq]
+map_rotr [lemma, in mathcomp.ssreflect.seq]
+map_rot [lemma, in mathcomp.ssreflect.seq]
+map_drop [lemma, in mathcomp.ssreflect.seq]
+map_take [lemma, in mathcomp.ssreflect.seq]
+map_rcons [lemma, in mathcomp.ssreflect.seq]
+map_cat [lemma, in mathcomp.ssreflect.seq]
+map_nseq [lemma, in mathcomp.ssreflect.seq]
+map_cons [lemma, in mathcomp.ssreflect.seq]
+map_preim [lemma, in mathcomp.ssreflect.fintype]
+map_cfAut_free [lemma, in mathcomp.character.classfun]
+map_orthogonal [lemma, in mathcomp.character.classfun]
+map_uniq_roots [lemma, in mathcomp.algebra.poly]
+map_diff_roots [lemma, in mathcomp.algebra.poly]
+map_poly_com [lemma, in mathcomp.algebra.poly]
+map_monic [lemma, in mathcomp.algebra.poly]
+map_poly_inj [lemma, in mathcomp.algebra.poly]
+map_poly_eq0 [lemma, in mathcomp.algebra.poly]
+map_comp_poly [lemma, in mathcomp.algebra.poly]
+map_polyC_eq0 [lemma, in mathcomp.algebra.poly]
+map_comm_coef [lemma, in mathcomp.algebra.poly]
+map_comm_poly [lemma, in mathcomp.algebra.poly]
+map_polyXn [lemma, in mathcomp.algebra.poly]
+map_polyX [lemma, in mathcomp.algebra.poly]
+map_polyZ [lemma, in mathcomp.algebra.poly]
+map_poly_is_rmorphism [lemma, in mathcomp.algebra.poly]
+map_polyC [lemma, in mathcomp.algebra.poly]
+map_poly_is_additive [lemma, in mathcomp.algebra.poly]
+map_poly_comp [lemma, in mathcomp.algebra.poly]
+map_Poly [lemma, in mathcomp.algebra.poly]
+map_polyK [lemma, in mathcomp.algebra.poly]
+map_inj_poly [lemma, in mathcomp.algebra.poly]
+map_poly_eq0_id0 [lemma, in mathcomp.algebra.poly]
+map_poly_comp_id0 [lemma, in mathcomp.algebra.poly]
+map_Poly_id0 [lemma, in mathcomp.algebra.poly]
+map_poly_id [lemma, in mathcomp.algebra.poly]
+map_poly0 [lemma, in mathcomp.algebra.poly]
+map_polyE [lemma, in mathcomp.algebra.poly]
+map_poly [definition, in mathcomp.algebra.poly]
+map_center_mx [lemma, in mathcomp.algebra.mxalgebra]
+map_cent_mx [lemma, in mathcomp.algebra.mxalgebra]
+map_mulsmx [lemma, in mathcomp.algebra.mxalgebra]
+map_eigenspace [lemma, in mathcomp.algebra.mxalgebra]
+map_diffmx [lemma, in mathcomp.algebra.mxalgebra]
+map_complmx [lemma, in mathcomp.algebra.mxalgebra]
+map_capmx [lemma, in mathcomp.algebra.mxalgebra]
+map_capmx_gen [lemma, in mathcomp.algebra.mxalgebra]
+map_addsmx [lemma, in mathcomp.algebra.mxalgebra]
+map_genmx [lemma, in mathcomp.algebra.mxalgebra]
+map_eqmx [lemma, in mathcomp.algebra.mxalgebra]
+map_ltmx [lemma, in mathcomp.algebra.mxalgebra]
+map_submx [lemma, in mathcomp.algebra.mxalgebra]
+map_cokermx [lemma, in mathcomp.algebra.mxalgebra]
+map_kermx [lemma, in mathcomp.algebra.mxalgebra]
+map_pinvmx [lemma, in mathcomp.algebra.mxalgebra]
+map_col_base [lemma, in mathcomp.algebra.mxalgebra]
+map_row_base [lemma, in mathcomp.algebra.mxalgebra]
+map_col_ebase [lemma, in mathcomp.algebra.mxalgebra]
+map_row_ebase [lemma, in mathcomp.algebra.mxalgebra]
+Map.f [variable, in mathcomp.ssreflect.seq]
+Map.n0 [variable, in mathcomp.ssreflect.seq]
+Map.T1 [variable, in mathcomp.ssreflect.seq]
+Map.T2 [variable, in mathcomp.ssreflect.seq]
+Map.x1 [variable, in mathcomp.ssreflect.seq]
+Map.x2 [variable, in mathcomp.ssreflect.seq]
+mask [definition, in mathcomp.ssreflect.seq]
+Mask [section, in mathcomp.ssreflect.seq]
+mask_subseq [lemma, in mathcomp.ssreflect.seq]
+mask_uniq [lemma, in mathcomp.ssreflect.seq]
+mask_rot [lemma, in mathcomp.ssreflect.seq]
+mask_cat [lemma, in mathcomp.ssreflect.seq]
+mask_cons [lemma, in mathcomp.ssreflect.seq]
+mask_true [lemma, in mathcomp.ssreflect.seq]
+mask_false [lemma, in mathcomp.ssreflect.seq]
+Mask.n0 [variable, in mathcomp.ssreflect.seq]
+Mask.T [variable, in mathcomp.ssreflect.seq]
+mask0 [lemma, in mathcomp.ssreflect.seq]
+mask1 [lemma, in mathcomp.ssreflect.seq]
+Matrix [constructor, in mathcomp.algebra.matrix]
+matrix [inductive, in mathcomp.algebra.matrix]
+matrix [library]
+MatrixAlgebra [section, in mathcomp.algebra.matrix]
+MatrixAlgebra [section, in mathcomp.algebra.mxalgebra]
+MatrixAlgebra.CentMxDef [section, in mathcomp.algebra.mxalgebra]
+MatrixAlgebra.CentMxDef.m [variable, in mathcomp.algebra.mxalgebra]
+MatrixAlgebra.CentMxDef.n [variable, in mathcomp.algebra.mxalgebra]
+MatrixAlgebra.CentMxDef.R [variable, in mathcomp.algebra.mxalgebra]
+MatrixAlgebra.F [variable, in mathcomp.algebra.mxalgebra]
+MatrixAlgebra.LiftPerm [section, in mathcomp.algebra.matrix]
+MatrixAlgebra.LiftPerm.n [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinMatrix [section, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinMatrix.f [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinMatrix.m1 [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinMatrix.m2 [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinMatrix.n1 [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinMatrix.n2 [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinRowVector [section, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinRowVector.f [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinRowVector.m [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.LinRowVector.n [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.MatrixRing [section, in mathcomp.algebra.matrix]
+MatrixAlgebra.MatrixRing.n' [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.Mulmxr [section, in mathcomp.algebra.matrix]
+MatrixAlgebra.Mulmxr.m [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.Mulmxr.n [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.Mulmxr.p [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.R [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.RingModule [section, in mathcomp.algebra.matrix]
+MatrixAlgebra.RingModule.m [variable, in mathcomp.algebra.matrix]
+MatrixAlgebra.RingModule.n [variable, in mathcomp.algebra.matrix]
+_ *m: _ (ring_scope) [notation, in mathcomp.algebra.matrix]
+MatrixAlgebra.ScalarMx [section, in mathcomp.algebra.matrix]
+MatrixAlgebra.ScalarMx.n [variable, in mathcomp.algebra.matrix]
+_ %:M (ring_scope) [notation, in mathcomp.algebra.matrix]
+MatrixAlgebra.StructuralLinear [section, in mathcomp.algebra.matrix]
+MatrixAlgebra.Trace [section, in mathcomp.algebra.matrix]
+MatrixAlgebra.Trace.n [variable, in mathcomp.algebra.matrix]
+\tr _ (ring_scope) [notation, in mathcomp.algebra.matrix]
+'Z ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
+'C ( _ ) (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
+_ * _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
+\tr _ (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ *m _ (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ %:M (ring_scope) [notation, in mathcomp.algebra.matrix]
+_ \in _ [notation, in mathcomp.algebra.mxalgebra]
+MatrixDef [section, in mathcomp.algebra.matrix]
+MatrixDef.m [variable, in mathcomp.algebra.matrix]
+MatrixDef.n [variable, in mathcomp.algebra.matrix]
+MatrixDef.R [variable, in mathcomp.algebra.matrix]
+MatrixDomain [section, in mathcomp.algebra.matrix]
+MatrixDomain.R [variable, in mathcomp.algebra.matrix]
+MatrixFormula [module, in mathcomp.algebra.mxpoly]
+MatrixFormula.Add [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.And [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.Bool [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_row_var [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_submx [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_col_mx [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_mxvec [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_vec_mx [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_mxrank [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_mulmx [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_mx_term [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_mx [definition, in mathcomp.algebra.mxpoly]
+MatrixFormula.Exists_rowP [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.Exists_row_form [definition, in mathcomp.algebra.mxpoly]
+MatrixFormula.False [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.form [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.holds [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula [section, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.Env [section, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.Env.d [variable, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.F [variable, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.Schur [variable, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.Subsetmx [section, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.Subsetmx.A [variable, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.Subsetmx.B [variable, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.Subsetmx.m1 [variable, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.Subsetmx.m2 [variable, in mathcomp.algebra.mxpoly]
+MatrixFormula.MatrixFormula.Subsetmx.n [variable, in mathcomp.algebra.mxpoly]
+MatrixFormula.morphAnd [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.mulmx_term [definition, in mathcomp.algebra.mxpoly]
+MatrixFormula.mxrank_form_qf [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.mxrank_form [definition, in mathcomp.algebra.mxpoly]
+MatrixFormula.mx_term [definition, in mathcomp.algebra.mxpoly]
+MatrixFormula.nth_row_env [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.nth_seq_of_rV [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.qf_eval [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.qf_form [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.row_env [definition, in mathcomp.algebra.mxpoly]
+MatrixFormula.row_var [definition, in mathcomp.algebra.mxpoly]
+MatrixFormula.seq_of_rV [definition, in mathcomp.algebra.mxpoly]
+MatrixFormula.size_seq_of_rV [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.submx_form_qf [lemma, in mathcomp.algebra.mxpoly]
+MatrixFormula.submx_form [definition, in mathcomp.algebra.mxpoly]
+MatrixFormula.term [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixFormula.True [abbreviation, in mathcomp.algebra.mxpoly]
+MatrixGenField [module, in mathcomp.character.mxrepresentation]
+MatrixGenField.Ad [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.Ad [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.base [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.base_full [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.base_free [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.Bool [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.card_gen [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.d [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.d [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField [section, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.A [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.Ad'T [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.cGA [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.d_gt0 [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.eval_mxT [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.F [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.G [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.gT [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.irrG [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.mulT [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.mxT [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.n' [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.DecideGenField.rG [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.eval_gen_term [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.eval_mulT [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.FA [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.FA [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.FA [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.False [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.FiniteGenField [section, in mathcomp.character.mxrepresentation]
+MatrixGenField.FiniteGenField.A [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.FiniteGenField.cGA [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.FiniteGenField.F [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.FiniteGenField.G [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.FiniteGenField.gT [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.FiniteGenField.irrG [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.FiniteGenField.n' [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.FiniteGenField.rG [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.form [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.Gen [constructor, in mathcomp.character.mxrepresentation]
+MatrixGenField.genD [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField [section, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.A [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.Bijection [section, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.Bijection.m1 [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.Bijection2 [section, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.Bijection2.m1 [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.cGA [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.d_gt0 [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.F [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.G [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.gT [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.inFA [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.irrG [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.n' [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.rG [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.GenField.val_genJmx [variable, in mathcomp.character.mxrepresentation]
+MatrixGenField.genK [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.genM [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.genN [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.genV [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_finMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_countMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_decFieldMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_satP [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_sat [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_form [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_env [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_term [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mx_irr [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mx_repr [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mx [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_dim_gt0 [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_dim_factor [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_base [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_dim [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_dim_ub_proof [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_dim_ex_proof [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_is_rmorphism [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_idomainMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_fieldMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_unitRingMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_invr0 [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mulVr [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_ringMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_ntriv [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mulDr [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mul1r [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mulC [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mulA [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_zmodMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_addNr [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_add0r [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_addC [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_addA [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_choiceMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_eqMixin [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_of [record, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen0 [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.gen1 [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.groot [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.inFA [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genJ [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.in_gen_row [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genZ [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.in_gen_sum [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genD [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genN [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.in_gen0 [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genK [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.in_gen [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.irr [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.m [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.map_mxminpoly_groot [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.morphAnd [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxmodule_rowval_gen [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxvalD [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxvalM [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxvalN [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxvalV [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_grootX [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_groot [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_centg [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_is_multiplicative [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_sub [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_genV [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_genM [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_gen1 [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_sum [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_inj [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval0 [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval1 [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.n [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.n [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.n [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.non_linear_gen_reducible [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.nth_map_rVval [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.pA [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.pval [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.rfix_gen [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.rGA [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.rker_gen [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.rowval_gen_stable [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.rowval_genK [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.rowval_gen [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.row_gen_sum_mxval [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.rstabs_rowval_gen [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.rstabs_in_gen [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.rstab_in_gen [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.rVval [projection, in mathcomp.character.mxrepresentation]
+MatrixGenField.sat_gen_form [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.set_nth_map_rVval [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.subbase [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.submx_rowval_gen [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.submx_in_gen_eq [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.submx_in_gen [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.term [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.True [abbreviation, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genJ [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genZ [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_gen_row [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_gen_rV [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_gen_sum [definition, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genD [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genN [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_gen0 [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genK [lemma, in mathcomp.character.mxrepresentation]
+MatrixGenField.val_gen [definition, in mathcomp.character.mxrepresentation]
+MatrixGroups [section, in mathcomp.character.mxabelem]
+MatrixInv [section, in mathcomp.algebra.matrix]
+MatrixInv.Defs [section, in mathcomp.algebra.matrix]
+MatrixInv.Defs.n [variable, in mathcomp.algebra.matrix]
+MatrixInv.n' [variable, in mathcomp.algebra.matrix]
+MatrixInv.R [variable, in mathcomp.algebra.matrix]
+matrixP [lemma, in mathcomp.algebra.matrix]
+MatrixStructural [section, in mathcomp.algebra.matrix]
+MatrixStructural.Block [section, in mathcomp.algebra.matrix]
+MatrixStructural.Block.CatBlock [section, in mathcomp.algebra.matrix]
+MatrixStructural.Block.CatBlock.A [variable, in mathcomp.algebra.matrix]
+MatrixStructural.Block.CatBlock.Adl [variable, in mathcomp.algebra.matrix]
+MatrixStructural.Block.CatBlock.Adr [variable, in mathcomp.algebra.matrix]
+MatrixStructural.Block.CatBlock.Aul [variable, in mathcomp.algebra.matrix]
+MatrixStructural.Block.CatBlock.Aur [variable, in mathcomp.algebra.matrix]
+MatrixStructural.Block.CutBlock [section, in mathcomp.algebra.matrix]
+MatrixStructural.Block.CutBlock.A [variable, in mathcomp.algebra.matrix]
+MatrixStructural.Block.m1 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.Block.m2 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.Block.n1 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.Block.n2 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.CutPaste [section, in mathcomp.algebra.matrix]
+MatrixStructural.CutPaste.m [variable, in mathcomp.algebra.matrix]
+MatrixStructural.CutPaste.m1 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.CutPaste.m2 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.CutPaste.n [variable, in mathcomp.algebra.matrix]
+MatrixStructural.CutPaste.n1 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.CutPaste.n2 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.FixedDim [section, in mathcomp.algebra.matrix]
+MatrixStructural.FixedDim.m [variable, in mathcomp.algebra.matrix]
+MatrixStructural.FixedDim.n [variable, in mathcomp.algebra.matrix]
+MatrixStructural.R [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrBlock [section, in mathcomp.algebra.matrix]
+MatrixStructural.TrBlock.Adl [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrBlock.Adr [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrBlock.Aul [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrBlock.Aur [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrBlock.m1 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrBlock.m2 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrBlock.n1 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrBlock.n2 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrCutBlock [section, in mathcomp.algebra.matrix]
+MatrixStructural.TrCutBlock.A [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrCutBlock.m1 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrCutBlock.m2 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrCutBlock.n1 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.TrCutBlock.n2 [variable, in mathcomp.algebra.matrix]
+MatrixStructural.VecMatrix [section, in mathcomp.algebra.matrix]
+MatrixStructural.VecMatrix.m [variable, in mathcomp.algebra.matrix]
+MatrixStructural.VecMatrix.n [variable, in mathcomp.algebra.matrix]
+_ ^T (ring_scope) [notation, in mathcomp.algebra.matrix]
+MatrixVectType [section, in mathcomp.algebra.vector]
+MatrixVectType.m [variable, in mathcomp.algebra.vector]
+MatrixVectType.n [variable, in mathcomp.algebra.vector]
+MatrixVectType.R [variable, in mathcomp.algebra.vector]
+MatrixZmodule [section, in mathcomp.algebra.matrix]
+MatrixZmodule.Additive [section, in mathcomp.algebra.matrix]
+MatrixZmodule.Additive.f [variable, in mathcomp.algebra.matrix]
+MatrixZmodule.Additive.g [variable, in mathcomp.algebra.matrix]
+MatrixZmodule.Additive.m [variable, in mathcomp.algebra.matrix]
+MatrixZmodule.Additive.n [variable, in mathcomp.algebra.matrix]
+MatrixZmodule.Additive.p [variable, in mathcomp.algebra.matrix]
+MatrixZmodule.Additive.q [variable, in mathcomp.algebra.matrix]
+MatrixZmodule.FixedDim [section, in mathcomp.algebra.matrix]
+MatrixZmodule.FixedDim.m [variable, in mathcomp.algebra.matrix]
+MatrixZmodule.FixedDim.n [variable, in mathcomp.algebra.matrix]
+MatrixZmodule.V [variable, in mathcomp.algebra.matrix]
+matrix_vectMixin [definition, in mathcomp.algebra.vector]
+matrix_vect_iso [lemma, in mathcomp.algebra.vector]
+matrix_unitRingMixin [definition, in mathcomp.algebra.matrix]
+matrix_ringMixin [definition, in mathcomp.algebra.matrix]
+matrix_nonzero1 [lemma, in mathcomp.algebra.matrix]
+matrix_sum_delta [lemma, in mathcomp.algebra.matrix]
+matrix_lmodMixin [definition, in mathcomp.algebra.matrix]
+matrix_zmodMixin [definition, in mathcomp.algebra.matrix]
+matrix_finMixin [definition, in mathcomp.algebra.matrix]
+matrix_countMixin [definition, in mathcomp.algebra.matrix]
+matrix_choiceMixin [definition, in mathcomp.algebra.matrix]
+matrix_eqMixin [definition, in mathcomp.algebra.matrix]
+matrix_of_fun [definition, in mathcomp.algebra.matrix]
+matrix_of_fun_def [definition, in mathcomp.algebra.matrix]
+matrix_key [lemma, in mathcomp.algebra.matrix]
+matrix_modr [lemma, in mathcomp.algebra.mxalgebra]
+matrix_modl [lemma, in mathcomp.algebra.mxalgebra]
+maxainv [definition, in mathcomp.solvable.jordanholder]
+maxainvM [lemma, in mathcomp.solvable.jordanholder]
+maxainvS [lemma, in mathcomp.solvable.jordanholder]
+maxainv_asimple_quo [lemma, in mathcomp.solvable.jordanholder]
+maxainv_exists [lemma, in mathcomp.solvable.jordanholder]
+maxainv_ainvar [lemma, in mathcomp.solvable.jordanholder]
+maxainv_sub [lemma, in mathcomp.solvable.jordanholder]
+maxainv_proper [lemma, in mathcomp.solvable.jordanholder]
+maxainv_norm [lemma, in mathcomp.solvable.jordanholder]
+maxgroup [definition, in mathcomp.fingroup.fingroup]
+maxgroupp [lemma, in mathcomp.fingroup.fingroup]
+maxgroupP [lemma, in mathcomp.fingroup.fingroup]
+maxgroup_exists [lemma, in mathcomp.fingroup.fingroup]
+maximal [definition, in mathcomp.solvable.gseries]
+maximal [library]
+maximalJ [lemma, in mathcomp.solvable.gseries]
+maximal_cycle_extremal [lemma, in mathcomp.solvable.extremal]
+maximal_eqJ [lemma, in mathcomp.solvable.gseries]
+maximal_exists [lemma, in mathcomp.solvable.gseries]
+maximal_eqP [lemma, in mathcomp.solvable.gseries]
+maximal_eq [definition, in mathcomp.solvable.gseries]
+maxKn [lemma, in mathcomp.ssreflect.ssrnat]
+maxminset [lemma, in mathcomp.ssreflect.finset]
+maxn [definition, in mathcomp.ssreflect.ssrnat]
+maxnA [lemma, in mathcomp.ssreflect.ssrnat]
+maxnAC [lemma, in mathcomp.ssreflect.ssrnat]
+maxnACA [lemma, in mathcomp.ssreflect.ssrnat]
+maxnC [lemma, in mathcomp.ssreflect.ssrnat]
+maxnCA [lemma, in mathcomp.ssreflect.ssrnat]
+maxnE [lemma, in mathcomp.ssreflect.ssrnat]
+maxnK [lemma, in mathcomp.ssreflect.ssrnat]
+maxnn [lemma, in mathcomp.ssreflect.ssrnat]
+maxnormal [definition, in mathcomp.solvable.gseries]
+maxnormalM [lemma, in mathcomp.solvable.gseries]
+MaxNormalProps [section, in mathcomp.solvable.gseries]
+MaxNormalProps.gT [variable, in mathcomp.solvable.gseries]
+maxnormal_minnormal [lemma, in mathcomp.solvable.gseries]
+maxnormal_sub [lemma, in mathcomp.solvable.gseries]
+maxnormal_proper [lemma, in mathcomp.solvable.gseries]
+maxnormal_normal [lemma, in mathcomp.solvable.gseries]
+maxnormal_charsimple [lemma, in mathcomp.solvable.maximal]
+maxnSS [lemma, in mathcomp.ssreflect.ssrnat]
+maxn_mull [lemma, in mathcomp.ssreflect.ssrnat]
+maxn_mulr [lemma, in mathcomp.ssreflect.ssrnat]
+maxn_minr [lemma, in mathcomp.ssreflect.ssrnat]
+maxn_minl [lemma, in mathcomp.ssreflect.ssrnat]
+maxn_idPr [lemma, in mathcomp.ssreflect.ssrnat]
+maxn_idPl [lemma, in mathcomp.ssreflect.ssrnat]
+maxn0 [lemma, in mathcomp.ssreflect.ssrnat]
+MaxProps [section, in mathcomp.solvable.gseries]
+MaxProps.gT [variable, in mathcomp.solvable.gseries]
+MaxRoots [section, in mathcomp.algebra.poly]
+MaxRoots.R [variable, in mathcomp.algebra.poly]
+maxset [definition, in mathcomp.ssreflect.finset]
+MaxSetMinSet [section, in mathcomp.ssreflect.finset]
+MaxSetMinSet.T [variable, in mathcomp.ssreflect.finset]
+maxsetp [lemma, in mathcomp.ssreflect.finset]
+maxsetP [lemma, in mathcomp.ssreflect.finset]
+maxsetsup [lemma, in mathcomp.ssreflect.finset]
+maxset_exists [lemma, in mathcomp.ssreflect.finset]
+maxset_eq [lemma, in mathcomp.ssreflect.finset]
+maxset_key [lemma, in mathcomp.ssreflect.finset]
+max_pgroupJ [lemma, in mathcomp.solvable.pgroup]
+max_pdiv_max [lemma, in mathcomp.ssreflect.prime]
+max_pdiv_gt0 [lemma, in mathcomp.ssreflect.prime]
+max_pdiv_leq [lemma, in mathcomp.ssreflect.prime]
+max_pdiv_dvd [lemma, in mathcomp.ssreflect.prime]
+max_pdiv_prime [lemma, in mathcomp.ssreflect.prime]
+max_pdiv [definition, in mathcomp.ssreflect.prime]
+max_size_mx_series [lemma, in mathcomp.character.mxrepresentation]
+max_submod_eqmx [lemma, in mathcomp.character.mxrepresentation]
+max_submodP [lemma, in mathcomp.character.mxrepresentation]
+max_submod [definition, in mathcomp.character.mxrepresentation]
+max_size_evalC [lemma, in mathcomp.algebra.polyXY]
+max_size_evalX [lemma, in mathcomp.algebra.polyXY]
+max_size_lead_coefXY [lemma, in mathcomp.algebra.polyXY]
+max_size_coefXY [lemma, in mathcomp.algebra.polyXY]
+max_cfRepr_mx1 [lemma, in mathcomp.character.character]
+max_cfRepr_norm_scalar [lemma, in mathcomp.character.character]
+max_card_abelian [lemma, in mathcomp.solvable.abelian]
+max_SCN [lemma, in mathcomp.solvable.maximal]
+max_card [lemma, in mathcomp.ssreflect.fintype]
+max_unity_roots [lemma, in mathcomp.algebra.poly]
+max_ring_poly_roots [lemma, in mathcomp.algebra.poly]
+max_poly_roots [lemma, in mathcomp.algebra.poly]
+max_pgroup_Sylow [lemma, in mathcomp.solvable.sylow]
+max0n [lemma, in mathcomp.ssreflect.ssrnat]
+meet_Ohm1 [lemma, in mathcomp.solvable.abelian]
+meet_center_nil [lemma, in mathcomp.solvable.nilpotent]
+memJ_norm [lemma, in mathcomp.fingroup.fingroup]
+memJ_class_support [lemma, in mathcomp.fingroup.fingroup]
+memJ_class [lemma, in mathcomp.fingroup.fingroup]
+memJ_conjg [lemma, in mathcomp.fingroup.fingroup]
+memmx_cent_envelop [lemma, in mathcomp.character.mxrepresentation]
+memmx_map [lemma, in mathcomp.algebra.mxalgebra]
+memmx_sumsP [lemma, in mathcomp.algebra.mxalgebra]
+memmx_addsP [lemma, in mathcomp.algebra.mxalgebra]
+memmx_eqP [lemma, in mathcomp.algebra.mxalgebra]
+memmx_subP [lemma, in mathcomp.algebra.mxalgebra]
+memmx0 [lemma, in mathcomp.algebra.mxalgebra]
+memmx1 [lemma, in mathcomp.algebra.mxalgebra]
+memPn [lemma, in mathcomp.ssreflect.eqtype]
+memPnC [lemma, in mathcomp.ssreflect.eqtype]
+mempx_Fadjoin [lemma, in mathcomp.field.fieldext]
+memtE [lemma, in mathcomp.ssreflect.tuple]
+memt_nth [lemma, in mathcomp.ssreflect.tuple]
+memvB [lemma, in mathcomp.algebra.vector]
+memvD [lemma, in mathcomp.algebra.vector]
+memvE [lemma, in mathcomp.algebra.vector]
+memvf [lemma, in mathcomp.algebra.vector]
+memvM [lemma, in mathcomp.field.falgebra]
+memvN [lemma, in mathcomp.algebra.vector]
+memvV [lemma, in mathcomp.field.falgebra]
+memvZ [lemma, in mathcomp.algebra.vector]
+memv_gal [lemma, in mathcomp.field.galois]
+memv_sum_pi [lemma, in mathcomp.algebra.vector]
+memv_projC [lemma, in mathcomp.algebra.vector]
+memv_pi2 [lemma, in mathcomp.algebra.vector]
+memv_pi1 [lemma, in mathcomp.algebra.vector]
+memv_proj [lemma, in mathcomp.algebra.vector]
+memv_pi [lemma, in mathcomp.algebra.vector]
+memv_preim [lemma, in mathcomp.algebra.vector]
+memv_ker [lemma, in mathcomp.algebra.vector]
+memv_imgP [lemma, in mathcomp.algebra.vector]
+memv_img [lemma, in mathcomp.algebra.vector]
+memv_span1 [lemma, in mathcomp.algebra.vector]
+memv_span [lemma, in mathcomp.algebra.vector]
+memv_capP [lemma, in mathcomp.algebra.vector]
+memv_cap [lemma, in mathcomp.algebra.vector]
+memv_sumP [lemma, in mathcomp.algebra.vector]
+memv_sumr [lemma, in mathcomp.algebra.vector]
+memv_addP [lemma, in mathcomp.algebra.vector]
+memv_add [lemma, in mathcomp.algebra.vector]
+memv_pick [lemma, in mathcomp.algebra.vector]
+memv_line [lemma, in mathcomp.algebra.vector]
+memv_suml [lemma, in mathcomp.algebra.vector]
+memv_submod_closed [lemma, in mathcomp.algebra.vector]
+memV_rcosetV [lemma, in mathcomp.fingroup.fingroup]
+memV_lcosetV [lemma, in mathcomp.fingroup.fingroup]
+memV_invg [lemma, in mathcomp.fingroup.fingroup]
+memv_adjoin [lemma, in mathcomp.field.falgebra]
+memv_cosetP [lemma, in mathcomp.field.falgebra]
+memv_algid [lemma, in mathcomp.field.falgebra]
+memv_mul [lemma, in mathcomp.field.falgebra]
+memv0 [lemma, in mathcomp.algebra.vector]
+mem_galNorm [lemma, in mathcomp.field.galois]
+mem_galTrace [lemma, in mathcomp.field.galois]
+mem_fixedFieldP [lemma, in mathcomp.field.galois]
+mem_Hall_pcore [lemma, in mathcomp.solvable.pgroup]
+mem_normal_Hall [lemma, in mathcomp.solvable.pgroup]
+mem_p_elt [lemma, in mathcomp.solvable.pgroup]
+mem_quotient [lemma, in mathcomp.fingroup.quotient]
+mem_repr_coset [lemma, in mathcomp.fingroup.quotient]
+mem_sort [lemma, in mathcomp.ssreflect.path]
+mem_merge [lemma, in mathcomp.ssreflect.path]
+mem_prev [lemma, in mathcomp.ssreflect.path]
+mem_next [lemma, in mathcomp.ssreflect.path]
+mem_zchar [lemma, in mathcomp.character.vcharacter]
+mem_zchar_on [lemma, in mathcomp.character.vcharacter]
+mem_baseVspace [lemma, in mathcomp.field.fieldext]
+mem_aspaceOver [lemma, in mathcomp.field.fieldext]
+mem_vspaceOver [lemma, in mathcomp.field.fieldext]
+mem_pcycle [lemma, in mathcomp.fingroup.perm]
+mem_primes [lemma, in mathcomp.ssreflect.prime]
+mem_prime_decomp [lemma, in mathcomp.ssreflect.prime]
+mem_sub_gring [lemma, in mathcomp.character.mxrepresentation]
+mem_gring_mx [lemma, in mathcomp.character.mxrepresentation]
+mem_bigdprod [lemma, in mathcomp.fingroup.gproduct]
+mem_dprod [lemma, in mathcomp.fingroup.gproduct]
+mem_sdprod [lemma, in mathcomp.fingroup.gproduct]
+mem_divgr [lemma, in mathcomp.fingroup.gproduct]
+mem_remgr [lemma, in mathcomp.fingroup.gproduct]
+mem_tnth [lemma, in mathcomp.ssreflect.tuple]
+mem_Cint_span [lemma, in mathcomp.field.algnum]
+mem_Crat_span [lemma, in mathcomp.field.algnum]
+mem_irr [lemma, in mathcomp.character.character]
+mem_allpairs [lemma, in mathcomp.ssreflect.seq]
+mem_iota [lemma, in mathcomp.ssreflect.seq]
+mem_pmap_sub [lemma, in mathcomp.ssreflect.seq]
+mem_pmap [lemma, in mathcomp.ssreflect.seq]
+mem_map [lemma, in mathcomp.ssreflect.seq]
+mem_rem_uniq [lemma, in mathcomp.ssreflect.seq]
+mem_rem [lemma, in mathcomp.ssreflect.seq]
+mem_subseq [lemma, in mathcomp.ssreflect.seq]
+mem_mask_rot [lemma, in mathcomp.ssreflect.seq]
+mem_mask [lemma, in mathcomp.ssreflect.seq]
+mem_mask_cons [lemma, in mathcomp.ssreflect.seq]
+mem_rotr [lemma, in mathcomp.ssreflect.seq]
+mem_rot [lemma, in mathcomp.ssreflect.seq]
+mem_undup [lemma, in mathcomp.ssreflect.seq]
+mem_rev [lemma, in mathcomp.ssreflect.seq]
+mem_filter [lemma, in mathcomp.ssreflect.seq]
+mem_drop [lemma, in mathcomp.ssreflect.seq]
+mem_take [lemma, in mathcomp.ssreflect.seq]
+mem_nth [lemma, in mathcomp.ssreflect.seq]
+mem_belast [lemma, in mathcomp.ssreflect.seq]
+mem_behead [lemma, in mathcomp.ssreflect.seq]
+mem_last [lemma, in mathcomp.ssreflect.seq]
+mem_head [lemma, in mathcomp.ssreflect.seq]
+mem_rcons [lemma, in mathcomp.ssreflect.seq]
+mem_cat [lemma, in mathcomp.ssreflect.seq]
+mem_seq4 [lemma, in mathcomp.ssreflect.seq]
+mem_seq3 [lemma, in mathcomp.ssreflect.seq]
+mem_seq2 [lemma, in mathcomp.ssreflect.seq]
+mem_seq1 [lemma, in mathcomp.ssreflect.seq]
+mem_seq [definition, in mathcomp.ssreflect.seq]
+mem_sum_enum [lemma, in mathcomp.ssreflect.fintype]
+mem_ord_enum [lemma, in mathcomp.ssreflect.fintype]
+mem_seq_sub_enum [lemma, in mathcomp.ssreflect.fintype]
+mem_sub_enum [lemma, in mathcomp.ssreflect.fintype]
+mem_image [lemma, in mathcomp.ssreflect.fintype]
+mem_iinv [lemma, in mathcomp.ssreflect.fintype]
+mem_enum [lemma, in mathcomp.ssreflect.fintype]
+mem_orbit [lemma, in mathcomp.fingroup.action]
+mem_setact [lemma, in mathcomp.fingroup.action]
+mem_unity_roots [lemma, in mathcomp.algebra.poly]
+mem_root [lemma, in mathcomp.algebra.poly]
+mem_index_enum [lemma, in mathcomp.ssreflect.bigop]
+mem_index_iota [lemma, in mathcomp.ssreflect.bigop]
+mem_rVabelem [lemma, in mathcomp.character.mxabelem]
+mem_im_abelem_rV [lemma, in mathcomp.character.mxabelem]
+mem_rowg [lemma, in mathcomp.character.mxabelem]
+mem_morphpre [lemma, in mathcomp.fingroup.morphism]
+mem_morphim [lemma, in mathcomp.fingroup.morphism]
+mem_cycle [lemma, in mathcomp.fingroup.fingroup]
+mem_commg [lemma, in mathcomp.fingroup.fingroup]
+mem_gen [lemma, in mathcomp.fingroup.fingroup]
+mem_class_support [lemma, in mathcomp.fingroup.fingroup]
+mem_repr_classes [lemma, in mathcomp.fingroup.fingroup]
+mem_lcosets [lemma, in mathcomp.fingroup.fingroup]
+mem_rcosets [lemma, in mathcomp.fingroup.fingroup]
+mem_repr_rcoset [lemma, in mathcomp.fingroup.fingroup]
+mem_classes [lemma, in mathcomp.fingroup.fingroup]
+mem_conjgV [lemma, in mathcomp.fingroup.fingroup]
+mem_conjg [lemma, in mathcomp.fingroup.fingroup]
+mem_rcoset [lemma, in mathcomp.fingroup.fingroup]
+mem_lcoset [lemma, in mathcomp.fingroup.fingroup]
+mem_invg [lemma, in mathcomp.fingroup.fingroup]
+mem_prodg [lemma, in mathcomp.fingroup.fingroup]
+mem_mulg [lemma, in mathcomp.fingroup.fingroup]
+mem_repr [lemma, in mathcomp.fingroup.fingroup]
+mem_closure [lemma, in mathcomp.ssreflect.fingraph]
+mem_Zp [lemma, in mathcomp.algebra.zmodp]
+mem_mulsmx [lemma, in mathcomp.algebra.mxalgebra]
+mem_pblock [lemma, in mathcomp.ssreflect.finset]
+mem_imset2 [lemma, in mathcomp.ssreflect.finset]
+mem_imset [lemma, in mathcomp.ssreflect.finset]
+mem0mx [lemma, in mathcomp.algebra.mxalgebra]
+mem0v [lemma, in mathcomp.algebra.vector]
+mem0_itvoo_xNx [lemma, in mathcomp.algebra.interval]
+mem0_itvcc_xNx [lemma, in mathcomp.algebra.interval]
+mem1v [lemma, in mathcomp.field.fieldext]
+mem2 [definition, in mathcomp.ssreflect.path]
+mem2l [lemma, in mathcomp.ssreflect.path]
+mem2lf [lemma, in mathcomp.ssreflect.path]
+mem2lr_splice [lemma, in mathcomp.ssreflect.path]
+mem2l_cat [lemma, in mathcomp.ssreflect.path]
+mem2r [lemma, in mathcomp.ssreflect.path]
+mem2rf [lemma, in mathcomp.ssreflect.path]
+mem2r_cat [lemma, in mathcomp.ssreflect.path]
+mem2_map [lemma, in mathcomp.ssreflect.path]
+mem2_last [lemma, in mathcomp.ssreflect.path]
+mem2_seq1 [lemma, in mathcomp.ssreflect.path]
+mem2_cons [lemma, in mathcomp.ssreflect.path]
+mem2_splice1 [lemma, in mathcomp.ssreflect.path]
+mem2_splice [lemma, in mathcomp.ssreflect.path]
+mem2_cat [lemma, in mathcomp.ssreflect.path]
+merge [definition, in mathcomp.ssreflect.path]
+merge_sort_rec [definition, in mathcomp.ssreflect.path]
+merge_sort_pop [definition, in mathcomp.ssreflect.path]
+merge_sort_push [definition, in mathcomp.ssreflect.path]
+merge_uniq [lemma, in mathcomp.ssreflect.path]
+merge_sorted [lemma, in mathcomp.ssreflect.path]
+merge_path [lemma, in mathcomp.ssreflect.path]
+metacyclic [definition, in mathcomp.solvable.cyclic]
+Metacyclic [section, in mathcomp.solvable.cyclic]
+metacyclicP [lemma, in mathcomp.solvable.cyclic]
+metacyclicS [lemma, in mathcomp.solvable.cyclic]
+metacyclic_sol [lemma, in mathcomp.solvable.nilpotent]
+Metacyclic.gT [variable, in mathcomp.solvable.cyclic]
+metacyclic1 [lemma, in mathcomp.solvable.cyclic]
+mfun [projection, in mathcomp.fingroup.morphism]
+mG [abbreviation, in mathcomp.character.mxrepresentation]
+Mho [definition, in mathcomp.solvable.abelian]
+MhoE [lemma, in mathcomp.solvable.abelian]
+MhoEabelian [lemma, in mathcomp.solvable.abelian]
+MhoJ [lemma, in mathcomp.solvable.abelian]
+MhoS [lemma, in mathcomp.solvable.abelian]
+Mho_leq [lemma, in mathcomp.solvable.abelian]
+Mho_normal [lemma, in mathcomp.solvable.abelian]
+Mho_char [lemma, in mathcomp.solvable.abelian]
+Mho_dprod [lemma, in mathcomp.solvable.abelian]
+Mho_cprod [lemma, in mathcomp.solvable.abelian]
+Mho_p_cycle [lemma, in mathcomp.solvable.abelian]
+Mho_cont [lemma, in mathcomp.solvable.abelian]
+Mho_sub [lemma, in mathcomp.solvable.abelian]
+Mho_p_elt [lemma, in mathcomp.solvable.abelian]
+Mho0 [lemma, in mathcomp.solvable.abelian]
+Mho1 [lemma, in mathcomp.solvable.abelian]
+mid [abbreviation, in mathcomp.algebra.interval]
+mid_in_itvcc [lemma, in mathcomp.algebra.interval]
+mid_in_itvoo [lemma, in mathcomp.algebra.interval]
+mid_in_itv [lemma, in mathcomp.algebra.interval]
+minCpolyP [lemma, in mathcomp.field.algC]
+minCpoly_aut [lemma, in mathcomp.field.algC]
+minCpoly_eq0 [lemma, in mathcomp.field.algC]
+minCpoly_monic [lemma, in mathcomp.field.algC]
+minCpoly_cyclotomic [lemma, in mathcomp.field.cyclotomic]
+mingroup [definition, in mathcomp.fingroup.fingroup]
+mingroupp [lemma, in mathcomp.fingroup.fingroup]
+mingroupP [lemma, in mathcomp.fingroup.fingroup]
+mingroup_exists [lemma, in mathcomp.fingroup.fingroup]
+minKn [lemma, in mathcomp.ssreflect.ssrnat]
+MinMaxGroup [section, in mathcomp.fingroup.fingroup]
+MinMaxGroup.G [variable, in mathcomp.fingroup.fingroup]
+MinMaxGroup.gP [variable, in mathcomp.fingroup.fingroup]
+MinMaxGroup.gPG [variable, in mathcomp.fingroup.fingroup]
+MinMaxGroup.gT [variable, in mathcomp.fingroup.fingroup]
+minmaxset [lemma, in mathcomp.ssreflect.finset]
+minn [definition, in mathcomp.ssreflect.ssrnat]
+minnA [lemma, in mathcomp.ssreflect.ssrnat]
+minnAC [lemma, in mathcomp.ssreflect.ssrnat]
+minnACA [lemma, in mathcomp.ssreflect.ssrnat]
+minnC [lemma, in mathcomp.ssreflect.ssrnat]
+minnCA [lemma, in mathcomp.ssreflect.ssrnat]
+minnE [lemma, in mathcomp.ssreflect.ssrnat]
+minnK [lemma, in mathcomp.ssreflect.ssrnat]
+minnn [lemma, in mathcomp.ssreflect.ssrnat]
+minnormal [definition, in mathcomp.solvable.gseries]
+minnormal_maxnormal [lemma, in mathcomp.solvable.gseries]
+minnormal_exists [lemma, in mathcomp.solvable.gseries]
+minnormal_solvable [lemma, in mathcomp.solvable.maximal]
+minnormal_charsimple [lemma, in mathcomp.solvable.maximal]
+minnSS [lemma, in mathcomp.ssreflect.ssrnat]
+minn_mull [lemma, in mathcomp.ssreflect.ssrnat]
+minn_mulr [lemma, in mathcomp.ssreflect.ssrnat]
+minn_maxr [lemma, in mathcomp.ssreflect.ssrnat]
+minn_maxl [lemma, in mathcomp.ssreflect.ssrnat]
+minn_idPr [lemma, in mathcomp.ssreflect.ssrnat]
+minn_idPl [lemma, in mathcomp.ssreflect.ssrnat]
+minn0 [lemma, in mathcomp.ssreflect.ssrnat]
+minPoly [definition, in mathcomp.field.fieldext]
+MinPoly [section, in mathcomp.algebra.mxpoly]
+minPolyOver [lemma, in mathcomp.field.fieldext]
+minPolyS [lemma, in mathcomp.field.fieldext]
+minPolyxx [lemma, in mathcomp.field.fieldext]
+minPoly_dvdp [lemma, in mathcomp.field.fieldext]
+minPoly_irr [lemma, in mathcomp.field.fieldext]
+minPoly_XsubC [lemma, in mathcomp.field.fieldext]
+minpoly_mx_ring [lemma, in mathcomp.algebra.mxpoly]
+minpoly_mxM [lemma, in mathcomp.algebra.mxpoly]
+minpoly_mx_free [lemma, in mathcomp.algebra.mxpoly]
+minpoly_mx1 [lemma, in mathcomp.algebra.mxpoly]
+minPoly_decidable_closure [lemma, in mathcomp.field.algebraics_fundamentals]
+MinPoly.A [variable, in mathcomp.algebra.mxpoly]
+MinPoly.F [variable, in mathcomp.algebra.mxpoly]
+MinPoly.n' [variable, in mathcomp.algebra.mxpoly]
+MinProps [section, in mathcomp.solvable.gseries]
+MinProps.gT [variable, in mathcomp.solvable.gseries]
+minset [definition, in mathcomp.ssreflect.finset]
+minsetinf [lemma, in mathcomp.ssreflect.finset]
+minsetp [lemma, in mathcomp.ssreflect.finset]
+minsetP [lemma, in mathcomp.ssreflect.finset]
+minset_exists [lemma, in mathcomp.ssreflect.finset]
+minset_eq [lemma, in mathcomp.ssreflect.finset]
+Mint_LmodMixin [definition, in mathcomp.algebra.ssrint]
+minusE [lemma, in mathcomp.ssreflect.ssrnat]
+min_subfx_vectAxiom [lemma, in mathcomp.field.fieldext]
+min_card_extraspecial [lemma, in mathcomp.solvable.maximal]
+min0n [lemma, in mathcomp.ssreflect.ssrnat]
+misom [definition, in mathcomp.fingroup.morphism]
+misomP [lemma, in mathcomp.fingroup.morphism]
+misom_isog [lemma, in mathcomp.fingroup.morphism]
+mker [lemma, in mathcomp.fingroup.morphism]
+mkerl [lemma, in mathcomp.fingroup.morphism]
+mkerr [lemma, in mathcomp.fingroup.morphism]
+mkfactors [definition, in mathcomp.solvable.jordanholder]
+mkFcube [definition, in mathcomp.solvable.burnside_app]
+MkIdeal [constructor, in mathcomp.algebra.ring_quotient]
+MkPrimeIdeal [constructor, in mathcomp.algebra.ring_quotient]
+mkRatio [constructor, in mathcomp.algebra.fraction]
+mkSec [definition, in mathcomp.solvable.jordanholder]
+mkseq [definition, in mathcomp.ssreflect.seq]
+mkseq_uniq [lemma, in mathcomp.ssreflect.seq]
+mkseq_nth [lemma, in mathcomp.ssreflect.seq]
+mksquare [definition, in mathcomp.solvable.burnside_app]
+mksrepr [definition, in mathcomp.solvable.jordanholder]
+mktuple [definition, in mathcomp.ssreflect.tuple]
+mk_mon [abbreviation, in mathcomp.algebra.mxpoly]
+Mmn [abbreviation, in mathcomp.character.mxabelem]
+modact [definition, in mathcomp.fingroup.action]
+modactE [lemma, in mathcomp.fingroup.action]
+modactEcond [lemma, in mathcomp.fingroup.action]
+ModAction [section, in mathcomp.fingroup.action]
+ModAction.aT [variable, in mathcomp.fingroup.action]
+ModAction.D [variable, in mathcomp.fingroup.action]
+ModAction.GenericMod [section, in mathcomp.fingroup.action]
+ModAction.GenericMod.acts_dom [variable, in mathcomp.fingroup.action]
+ModAction.GenericMod.H [variable, in mathcomp.fingroup.action]
+ModAction.GenericMod.Stabilizers [section, in mathcomp.fingroup.action]
+ModAction.GenericMod.Stabilizers.cSH [variable, in mathcomp.fingroup.action]
+ModAction.GenericMod.Stabilizers.fixSH [variable, in mathcomp.fingroup.action]
+ModAction.GenericMod.Stabilizers.S [variable, in mathcomp.fingroup.action]
+ModAction.rT [variable, in mathcomp.fingroup.action]
+ModAction.to [variable, in mathcomp.fingroup.action]
+modact_coset_astab [lemma, in mathcomp.fingroup.action]
+modact_is_groupAction [lemma, in mathcomp.fingroup.action]
+modact_faithful [lemma, in mathcomp.fingroup.action]
+modact_is_action [lemma, in mathcomp.fingroup.action]
+modG [abbreviation, in mathcomp.character.mxrepresentation]
+modgactE [lemma, in mathcomp.fingroup.action]
+modn [definition, in mathcomp.ssreflect.div]
+modnDl [lemma, in mathcomp.ssreflect.div]
+modnDm [lemma, in mathcomp.ssreflect.div]
+modnDml [lemma, in mathcomp.ssreflect.div]
+modnDmr [lemma, in mathcomp.ssreflect.div]
+modnDr [lemma, in mathcomp.ssreflect.div]
+modnMDl [lemma, in mathcomp.ssreflect.div]
+modnMl [lemma, in mathcomp.ssreflect.div]
+modnMm [lemma, in mathcomp.ssreflect.div]
+modnMml [lemma, in mathcomp.ssreflect.div]
+modnMmr [lemma, in mathcomp.ssreflect.div]
+modnMr [lemma, in mathcomp.ssreflect.div]
+modnn [lemma, in mathcomp.ssreflect.div]
+modnXm [lemma, in mathcomp.ssreflect.div]
+modNz_nat [lemma, in mathcomp.algebra.intdiv]
+modn_summ [lemma, in mathcomp.ssreflect.binomial]
+modn_partP [lemma, in mathcomp.ssreflect.prime]
+modn_coprime [lemma, in mathcomp.ssreflect.div]
+modn_dvdm [lemma, in mathcomp.ssreflect.div]
+modn_mod [lemma, in mathcomp.ssreflect.div]
+modn_small [lemma, in mathcomp.ssreflect.div]
+modn_def [lemma, in mathcomp.ssreflect.div]
+modn_rec [definition, in mathcomp.ssreflect.div]
+modn0 [lemma, in mathcomp.ssreflect.div]
+modn1 [lemma, in mathcomp.ssreflect.div]
+modn2 [lemma, in mathcomp.ssreflect.div]
+ModP [section, in mathcomp.solvable.sylow]
+modp_polyOver [lemma, in mathcomp.field.fieldext]
+ModP.aT [variable, in mathcomp.solvable.sylow]
+ModP.D [variable, in mathcomp.solvable.sylow]
+ModP.sT [variable, in mathcomp.solvable.sylow]
+ModP.to [variable, in mathcomp.solvable.sylow]
+ModularGroup [constructor, in mathcomp.solvable.extremal]
+ModularGroupAction [section, in mathcomp.solvable.sylow]
+ModularGroupAction.aT [variable, in mathcomp.solvable.sylow]
+ModularGroupAction.D [variable, in mathcomp.solvable.sylow]
+ModularGroupAction.p [variable, in mathcomp.solvable.sylow]
+ModularGroupAction.R [variable, in mathcomp.solvable.sylow]
+ModularGroupAction.rT [variable, in mathcomp.solvable.sylow]
+ModularGroupAction.to [variable, in mathcomp.solvable.sylow]
+ModularRepresentation [section, in mathcomp.character.mxabelem]
+ModularRepresentation.charFp [variable, in mathcomp.character.mxabelem]
+ModularRepresentation.F [variable, in mathcomp.character.mxabelem]
+ModularRepresentation.G [variable, in mathcomp.character.mxabelem]
+ModularRepresentation.gT [variable, in mathcomp.character.mxabelem]
+ModularRepresentation.n [variable, in mathcomp.character.mxabelem]
+ModularRepresentation.p [variable, in mathcomp.character.mxabelem]
+ModularRepresentation.rG [variable, in mathcomp.character.mxabelem]
+modular_group_classP [lemma, in mathcomp.solvable.extremal]
+modular_group_structure [lemma, in mathcomp.solvable.extremal]
+modular_group_generators [definition, in mathcomp.solvable.extremal]
+modular_gtype [definition, in mathcomp.solvable.extremal]
+module_baseAspace [lemma, in mathcomp.field.fieldext]
+module_baseVspace [lemma, in mathcomp.field.fieldext]
+modz [definition, in mathcomp.algebra.intdiv]
+modzDl [lemma, in mathcomp.algebra.intdiv]
+modzDm [lemma, in mathcomp.algebra.intdiv]
+modzDml [lemma, in mathcomp.algebra.intdiv]
+modzDmr [lemma, in mathcomp.algebra.intdiv]
+modzDr [lemma, in mathcomp.algebra.intdiv]
+modzMDl [lemma, in mathcomp.algebra.intdiv]
+modzMl [lemma, in mathcomp.algebra.intdiv]
+modzMm [lemma, in mathcomp.algebra.intdiv]
+modzMml [lemma, in mathcomp.algebra.intdiv]
+modzMmr [lemma, in mathcomp.algebra.intdiv]
+modzMr [lemma, in mathcomp.algebra.intdiv]
+modzN [lemma, in mathcomp.algebra.intdiv]
+modzNm [lemma, in mathcomp.algebra.intdiv]
+modZp [lemma, in mathcomp.algebra.zmodp]
+modzXm [lemma, in mathcomp.algebra.intdiv]
+modzz [lemma, in mathcomp.algebra.intdiv]
+modz_absm [lemma, in mathcomp.algebra.intdiv]
+modz_mod [lemma, in mathcomp.algebra.intdiv]
+modz_small [lemma, in mathcomp.algebra.intdiv]
+modz_ge0 [lemma, in mathcomp.algebra.intdiv]
+modz_nat [lemma, in mathcomp.algebra.intdiv]
+modz_abs [lemma, in mathcomp.algebra.intdiv]
+modz0 [lemma, in mathcomp.algebra.intdiv]
+modz1 [lemma, in mathcomp.algebra.intdiv]
+mod_Iirr_bij [lemma, in mathcomp.character.character]
+mod_IirrK [lemma, in mathcomp.character.character]
+mod_Iirr_eq0 [lemma, in mathcomp.character.character]
+mod_IirrE [lemma, in mathcomp.character.character]
+mod_Iirr0 [lemma, in mathcomp.character.character]
+mod_Iirr [definition, in mathcomp.character.character]
+mod0n [lemma, in mathcomp.ssreflect.div]
+mod0z [lemma, in mathcomp.algebra.intdiv]
+monic [definition, in mathcomp.algebra.poly]
+monicE [lemma, in mathcomp.algebra.poly]
+monicMl [lemma, in mathcomp.algebra.poly]
+monicMr [lemma, in mathcomp.algebra.poly]
+monicP [lemma, in mathcomp.algebra.poly]
+monicX [lemma, in mathcomp.algebra.poly]
+monicXn [lemma, in mathcomp.algebra.poly]
+monicXsubC [lemma, in mathcomp.algebra.poly]
+monic_minPoly [lemma, in mathcomp.field.fieldext]
+monic_map [lemma, in mathcomp.algebra.poly]
+monic_Xn_sub_1 [lemma, in mathcomp.algebra.poly]
+monic_comreg [lemma, in mathcomp.algebra.poly]
+monic_prod_XsubC [lemma, in mathcomp.algebra.poly]
+monic_prod [lemma, in mathcomp.algebra.poly]
+monic_exp [lemma, in mathcomp.algebra.poly]
+monic_mulr_closed [lemma, in mathcomp.algebra.poly]
+monic_neq0 [lemma, in mathcomp.algebra.poly]
+monic_key [lemma, in mathcomp.algebra.poly]
+monic1 [lemma, in mathcomp.algebra.poly]
+Monoid [module, in mathcomp.ssreflect.bigop]
+MonoidProperties [section, in mathcomp.ssreflect.bigop]
+MonoidProperties.Abelian [section, in mathcomp.ssreflect.bigop]
+MonoidProperties.Abelian.op [variable, in mathcomp.ssreflect.bigop]
+_ * _ [notation, in mathcomp.ssreflect.bigop]
+*%M [notation, in mathcomp.ssreflect.bigop]
+MonoidProperties.idx [variable, in mathcomp.ssreflect.bigop]
+MonoidProperties.Plain [section, in mathcomp.ssreflect.bigop]
+MonoidProperties.Plain.op [variable, in mathcomp.ssreflect.bigop]
+_ * _ [notation, in mathcomp.ssreflect.bigop]
+*%M [notation, in mathcomp.ssreflect.bigop]
+MonoidProperties.R [variable, in mathcomp.ssreflect.bigop]
+1 [notation, in mathcomp.ssreflect.bigop]
+Monoid.AddLaw [constructor, in mathcomp.ssreflect.bigop]
+Monoid.add_operator [projection, in mathcomp.ssreflect.bigop]
+Monoid.add_law [record, in mathcomp.ssreflect.bigop]
+Monoid.clone_add_law [definition, in mathcomp.ssreflect.bigop]
+Monoid.clone_mul_law [definition, in mathcomp.ssreflect.bigop]
+Monoid.clone_com_law [definition, in mathcomp.ssreflect.bigop]
+Monoid.clone_law [definition, in mathcomp.ssreflect.bigop]
+Monoid.ComLaw [constructor, in mathcomp.ssreflect.bigop]
+Monoid.CommutativeAxioms [section, in mathcomp.ssreflect.bigop]
+Monoid.CommutativeAxioms.add [variable, in mathcomp.ssreflect.bigop]
+Monoid.CommutativeAxioms.inv [variable, in mathcomp.ssreflect.bigop]
+Monoid.CommutativeAxioms.mul [variable, in mathcomp.ssreflect.bigop]
+Monoid.CommutativeAxioms.mulC [variable, in mathcomp.ssreflect.bigop]
+Monoid.CommutativeAxioms.one [variable, in mathcomp.ssreflect.bigop]
+Monoid.CommutativeAxioms.T [variable, in mathcomp.ssreflect.bigop]
+Monoid.CommutativeAxioms.zero [variable, in mathcomp.ssreflect.bigop]
+Monoid.com_operator [projection, in mathcomp.ssreflect.bigop]
+Monoid.com_law [record, in mathcomp.ssreflect.bigop]
+Monoid.Definitions [section, in mathcomp.ssreflect.bigop]
+Monoid.Definitions.idm [variable, in mathcomp.ssreflect.bigop]
+Monoid.Definitions.op_id [variable, in mathcomp.ssreflect.bigop]
+Monoid.Definitions.T [variable, in mathcomp.ssreflect.bigop]
+Monoid.Exports [module, in mathcomp.ssreflect.bigop]
+[ add_law _ of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
+[ mul_law of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
+[ com_law of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
+[ law of _ ] (form_scope) [notation, in mathcomp.ssreflect.bigop]
+Monoid.law [record, in mathcomp.ssreflect.bigop]
+Monoid.Law [constructor, in mathcomp.ssreflect.bigop]
+Monoid.mulC_dist [lemma, in mathcomp.ssreflect.bigop]
+Monoid.mulC_zero [lemma, in mathcomp.ssreflect.bigop]
+Monoid.mulC_id [lemma, in mathcomp.ssreflect.bigop]
+Monoid.MulLaw [constructor, in mathcomp.ssreflect.bigop]
+Monoid.mul_operator [projection, in mathcomp.ssreflect.bigop]
+Monoid.mul_law [record, in mathcomp.ssreflect.bigop]
+Monoid.operator [projection, in mathcomp.ssreflect.bigop]
+Monoid.Theory [module, in mathcomp.ssreflect.bigop]
+Monoid.Theory.addmA [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.addmAC [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.addmC [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.addmCA [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.addm0 [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.add0m [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.iteropE [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmA [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmAC [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmACA [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmC [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmCA [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulm_addr [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulm_addl [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulm0 [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulm1 [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mul0m [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.mul1m [lemma, in mathcomp.ssreflect.bigop]
+Monoid.Theory.simpm [definition, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory [section, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.Add [section, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.Add.add [variable, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.Add.mul [variable, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.Commutative [section, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.Commutative.mul [variable, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.idm [variable, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.Mul [section, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.Mul.mul [variable, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.Plain [section, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.Plain.mul [variable, in mathcomp.ssreflect.bigop]
+Monoid.Theory.Theory.T [variable, in mathcomp.ssreflect.bigop]
+MonotonicFunctorTheory [section, in mathcomp.solvable.gfunctor]
+MonotonicFunctorTheory.Composition [section, in mathcomp.solvable.gfunctor]
+MonotonicFunctorTheory.Composition.F1 [variable, in mathcomp.solvable.gfunctor]
+MonotonicFunctorTheory.Composition.F2 [variable, in mathcomp.solvable.gfunctor]
+MonotonicFunctorTheory.F1 [variable, in mathcomp.solvable.gfunctor]
+MonotonicFunctorTheory.F2 [variable, in mathcomp.solvable.gfunctor]
+mono_leqif [lemma, in mathcomp.ssreflect.ssrnat]
+MoreAlgCaut [section, in mathcomp.field.algnum]
+MoreConstt [section, in mathcomp.character.character]
+MoreConstt.G [variable, in mathcomp.character.character]
+MoreConstt.gT [variable, in mathcomp.character.character]
+MoreConstt.H [variable, in mathcomp.character.character]
+MoreCoset [section, in mathcomp.character.classfun]
+MoreCoset.G [variable, in mathcomp.character.classfun]
+MoreCoset.gT [variable, in mathcomp.character.classfun]
+MoreFieldOver [section, in mathcomp.field.fieldext]
+MoreFieldOver.F [variable, in mathcomp.field.fieldext]
+MoreFieldOver.F0 [variable, in mathcomp.field.fieldext]
+MoreFieldOver.L [variable, in mathcomp.field.fieldext]
+MoreGroupAction [section, in mathcomp.solvable.jordanholder]
+MoreGroupAction.A [variable, in mathcomp.solvable.jordanholder]
+MoreGroupAction.aT [variable, in mathcomp.solvable.jordanholder]
+MoreGroupAction.D [variable, in mathcomp.solvable.jordanholder]
+MoreGroupAction.rT [variable, in mathcomp.solvable.jordanholder]
+MoreGroupAction.to [variable, in mathcomp.solvable.jordanholder]
+MoreInertia [section, in mathcomp.character.inertia]
+MoreInertia.G [variable, in mathcomp.character.inertia]
+MoreInertia.gT [variable, in mathcomp.character.inertia]
+MoreInertia.H [variable, in mathcomp.character.inertia]
+MoreInertia.i [variable, in mathcomp.character.inertia]
+MoreInertia.T [variable, in mathcomp.character.inertia]
+MoreIntegralChar [section, in mathcomp.character.integral_char]
+MoreQuotientAction [section, in mathcomp.solvable.jordanholder]
+MoreQuotientAction.A [variable, in mathcomp.solvable.jordanholder]
+MoreQuotientAction.aT [variable, in mathcomp.solvable.jordanholder]
+MoreQuotientAction.D [variable, in mathcomp.solvable.jordanholder]
+MoreQuotientAction.rT [variable, in mathcomp.solvable.jordanholder]
+MoreQuotientAction.to [variable, in mathcomp.solvable.jordanholder]
+MoreRestrict [section, in mathcomp.character.classfun]
+MoreRestrict.G [variable, in mathcomp.character.classfun]
+MoreRestrict.gT [variable, in mathcomp.character.classfun]
+MoreRestrict.H [variable, in mathcomp.character.classfun]
+MoreSgz [section, in mathcomp.algebra.ssrint]
+MoreSgz.R [variable, in mathcomp.algebra.ssrint]
+MoreSylow [section, in mathcomp.solvable.sylow]
+MoreSylow.gT [variable, in mathcomp.solvable.sylow]
+MoreSylow.p [variable, in mathcomp.solvable.sylow]
+MoreVchar [section, in mathcomp.character.vcharacter]
+MoreVchar.G [variable, in mathcomp.character.vcharacter]
+MoreVchar.gT [variable, in mathcomp.character.vcharacter]
+MoreVchar.H [variable, in mathcomp.character.vcharacter]
+MorphAbelem [section, in mathcomp.solvable.abelian]
+MorphAbelem.aT [variable, in mathcomp.solvable.abelian]
+MorphAbelem.D [variable, in mathcomp.solvable.abelian]
+MorphAbelem.f [variable, in mathcomp.solvable.abelian]
+MorphAbelem.rT [variable, in mathcomp.solvable.abelian]
+MorphAct [section, in mathcomp.fingroup.action]
+MorphAction [section, in mathcomp.fingroup.action]
+MorphAction.A [variable, in mathcomp.fingroup.action]
+MorphAction.actsDR [variable, in mathcomp.fingroup.action]
+MorphAction.aT1 [variable, in mathcomp.fingroup.action]
+MorphAction.aT2 [variable, in mathcomp.fingroup.action]
+MorphAction.defD2 [variable, in mathcomp.fingroup.action]
+MorphAction.D1 [variable, in mathcomp.fingroup.action]
+MorphAction.D2 [variable, in mathcomp.fingroup.action]
+MorphAction.f [variable, in mathcomp.fingroup.action]
+MorphAction.h [variable, in mathcomp.fingroup.action]
+MorphAction.hfJ [variable, in mathcomp.fingroup.action]
+MorphAction.injh [variable, in mathcomp.fingroup.action]
+MorphAction.R [variable, in mathcomp.fingroup.action]
+MorphAction.rT1 [variable, in mathcomp.fingroup.action]
+MorphAction.rT2 [variable, in mathcomp.fingroup.action]
+MorphAction.S [variable, in mathcomp.fingroup.action]
+MorphAction.sAD1 [variable, in mathcomp.fingroup.action]
+MorphAction.sSR [variable, in mathcomp.fingroup.action]
+MorphAction.to1 [variable, in mathcomp.fingroup.action]
+MorphAction.to2 [variable, in mathcomp.fingroup.action]
+MorphAct.aT [variable, in mathcomp.fingroup.action]
+MorphAct.D [variable, in mathcomp.fingroup.action]
+MorphAct.phi [variable, in mathcomp.fingroup.action]
+MorphAct.rT [variable, in mathcomp.fingroup.action]
+morphAnd [abbreviation, in mathcomp.character.mxrepresentation]
+MorPhantom [definition, in mathcomp.fingroup.morphism]
+morPhantom [abbreviation, in mathcomp.fingroup.morphism]
+MorphGroupAction [section, in mathcomp.fingroup.action]
+MorphGroupAction.aT1 [variable, in mathcomp.fingroup.action]
+MorphGroupAction.aT2 [variable, in mathcomp.fingroup.action]
+MorphGroupAction.D1 [variable, in mathcomp.fingroup.action]
+MorphGroupAction.D2 [variable, in mathcomp.fingroup.action]
+MorphGroupAction.f [variable, in mathcomp.fingroup.action]
+MorphGroupAction.h [variable, in mathcomp.fingroup.action]
+MorphGroupAction.hfJ [variable, in mathcomp.fingroup.action]
+MorphGroupAction.iso_f [variable, in mathcomp.fingroup.action]
+MorphGroupAction.iso_h [variable, in mathcomp.fingroup.action]
+MorphGroupAction.rT1 [variable, in mathcomp.fingroup.action]
+MorphGroupAction.rT2 [variable, in mathcomp.fingroup.action]
+MorphGroupAction.R1 [variable, in mathcomp.fingroup.action]
+MorphGroupAction.R2 [variable, in mathcomp.fingroup.action]
+MorphGroupAction.to1 [variable, in mathcomp.fingroup.action]
+MorphGroupAction.to2 [variable, in mathcomp.fingroup.action]
+morphic [definition, in mathcomp.fingroup.morphism]
+MorphicImage [section, in mathcomp.solvable.cyclic]
+MorphicImage.aT [variable, in mathcomp.solvable.cyclic]
+MorphicImage.D [variable, in mathcomp.solvable.cyclic]
+MorphicImage.Dx [variable, in mathcomp.solvable.cyclic]
+MorphicImage.f [variable, in mathcomp.solvable.cyclic]
+MorphicImage.rT [variable, in mathcomp.solvable.cyclic]
+MorphicImage.x [variable, in mathcomp.solvable.cyclic]
+morphicP [lemma, in mathcomp.fingroup.morphism]
+morphic_aut [lemma, in mathcomp.fingroup.automorphism]
+Morphim [section, in mathcomp.solvable.pgroup]
+Morphim [section, in mathcomp.character.character]
+Morphim [section, in mathcomp.character.classfun]
+morphim [definition, in mathcomp.fingroup.morphism]
+morphimD [lemma, in mathcomp.fingroup.morphism]
+morphimDG [lemma, in mathcomp.fingroup.morphism]
+morphimD1 [lemma, in mathcomp.fingroup.morphism]
+morphimE [lemma, in mathcomp.fingroup.morphism]
+morphimEdom [lemma, in mathcomp.fingroup.morphism]
+morphimEsub [lemma, in mathcomp.fingroup.morphism]
+morphimF [lemma, in mathcomp.solvable.gfunctor]
+morphimGI [lemma, in mathcomp.fingroup.morphism]
+morphimGK [lemma, in mathcomp.fingroup.morphism]
+morphimI [lemma, in mathcomp.fingroup.morphism]
+morphimIdom [lemma, in mathcomp.fingroup.morphism]
+morphimIG [lemma, in mathcomp.fingroup.morphism]
+morphimIim [lemma, in mathcomp.fingroup.morphism]
+MorphimInternalProd [section, in mathcomp.fingroup.gproduct]
+MorphimInternalProd.D [variable, in mathcomp.fingroup.gproduct]
+MorphimInternalProd.f [variable, in mathcomp.fingroup.gproduct]
+MorphimInternalProd.gT [variable, in mathcomp.fingroup.gproduct]
+MorphimInternalProd.OneProd [section, in mathcomp.fingroup.gproduct]
+MorphimInternalProd.OneProd.G [variable, in mathcomp.fingroup.gproduct]
+MorphimInternalProd.OneProd.H [variable, in mathcomp.fingroup.gproduct]
+MorphimInternalProd.OneProd.K [variable, in mathcomp.fingroup.gproduct]
+MorphimInternalProd.OneProd.sGD [variable, in mathcomp.fingroup.gproduct]
+MorphimInternalProd.rT [variable, in mathcomp.fingroup.gproduct]
+morphimJ [lemma, in mathcomp.fingroup.morphism]
+morphimK [lemma, in mathcomp.fingroup.morphism]
+morphimMl [lemma, in mathcomp.fingroup.morphism]
+morphimMr [lemma, in mathcomp.fingroup.morphism]
+morphimP [lemma, in mathcomp.fingroup.morphism]
+morphimR [lemma, in mathcomp.fingroup.morphism]
+morphimS [lemma, in mathcomp.fingroup.morphism]
+morphimSGK [lemma, in mathcomp.fingroup.morphism]
+morphimSK [lemma, in mathcomp.fingroup.morphism]
+MorphimSpec [constructor, in mathcomp.fingroup.morphism]
+morphimT [lemma, in mathcomp.fingroup.morphism]
+morphimU [lemma, in mathcomp.fingroup.morphism]
+morphimV [lemma, in mathcomp.fingroup.morphism]
+morphimY [lemma, in mathcomp.fingroup.morphism]
+morphim_pseries [lemma, in mathcomp.solvable.pgroup]
+morphim_pcore_mod [lemma, in mathcomp.solvable.pgroup]
+morphim_pcore [lemma, in mathcomp.solvable.pgroup]
+morphim_Sylow [lemma, in mathcomp.solvable.pgroup]
+morphim_p_group [lemma, in mathcomp.solvable.pgroup]
+morphim_pSylow [lemma, in mathcomp.solvable.pgroup]
+morphim_Hall [lemma, in mathcomp.solvable.pgroup]
+morphim_pHall [lemma, in mathcomp.solvable.pgroup]
+morphim_p_index [lemma, in mathcomp.solvable.pgroup]
+morphim_odd [lemma, in mathcomp.solvable.pgroup]
+morphim_pgroup [lemma, in mathcomp.solvable.pgroup]
+morphim_qisom_inj [lemma, in mathcomp.fingroup.quotient]
+morphim_qisom [lemma, in mathcomp.fingroup.quotient]
+morphim_quotm [lemma, in mathcomp.fingroup.quotient]
+morphim_mx_abs_irr [lemma, in mathcomp.character.mxrepresentation]
+morphim_mx_irr [lemma, in mathcomp.character.mxrepresentation]
+morphim_mx_repr [lemma, in mathcomp.character.mxrepresentation]
+morphim_mxE [lemma, in mathcomp.character.mxrepresentation]
+morphim_mx [definition, in mathcomp.character.mxrepresentation]
+morphim_dprodmr [lemma, in mathcomp.fingroup.gproduct]
+morphim_dprodml [lemma, in mathcomp.fingroup.gproduct]
+morphim_dprodm [lemma, in mathcomp.fingroup.gproduct]
+morphim_cprodmr [lemma, in mathcomp.fingroup.gproduct]
+morphim_cprodml [lemma, in mathcomp.fingroup.gproduct]
+morphim_cprodm [lemma, in mathcomp.fingroup.gproduct]
+morphim_sdprodmr [lemma, in mathcomp.fingroup.gproduct]
+morphim_sdprodml [lemma, in mathcomp.fingroup.gproduct]
+morphim_sdprodm [lemma, in mathcomp.fingroup.gproduct]
+morphim_pprodmr [lemma, in mathcomp.fingroup.gproduct]
+morphim_pprodml [lemma, in mathcomp.fingroup.gproduct]
+morphim_pprodm [lemma, in mathcomp.fingroup.gproduct]
+morphim_sndX [lemma, in mathcomp.fingroup.gproduct]
+morphim_fstX [lemma, in mathcomp.fingroup.gproduct]
+morphim_pair1g [lemma, in mathcomp.fingroup.gproduct]
+morphim_pairg1 [lemma, in mathcomp.fingroup.gproduct]
+morphim_coprime_bigdprod [lemma, in mathcomp.fingroup.gproduct]
+morphim_bigcprod [lemma, in mathcomp.fingroup.gproduct]
+morphim_coprime_dprod [lemma, in mathcomp.fingroup.gproduct]
+morphim_cprod [lemma, in mathcomp.fingroup.gproduct]
+morphim_coprime_sdprod [lemma, in mathcomp.fingroup.gproduct]
+morphim_pprod [lemma, in mathcomp.fingroup.gproduct]
+morphim_conj [lemma, in mathcomp.fingroup.automorphism]
+morphim_fixP [lemma, in mathcomp.fingroup.automorphism]
+morphim_p_rank_abelian [lemma, in mathcomp.solvable.abelian]
+morphim_rank_abelian [lemma, in mathcomp.solvable.abelian]
+morphim_Ohm [lemma, in mathcomp.solvable.abelian]
+morphim_Mho [lemma, in mathcomp.solvable.abelian]
+morphim_grank [lemma, in mathcomp.solvable.abelian]
+morphim_pnElem [lemma, in mathcomp.solvable.abelian]
+morphim_pElem [lemma, in mathcomp.solvable.abelian]
+morphim_abelem [lemma, in mathcomp.solvable.abelian]
+morphim_Ldiv [lemma, in mathcomp.solvable.abelian]
+morphim_LdivT [lemma, in mathcomp.solvable.abelian]
+morphim_subnormal [lemma, in mathcomp.solvable.gseries]
+morphim_Fitting [lemma, in mathcomp.solvable.maximal]
+morphim_Phi [lemma, in mathcomp.solvable.maximal]
+morphim_actm [lemma, in mathcomp.fingroup.action]
+morphim_sol [lemma, in mathcomp.solvable.nilpotent]
+morphim_nil [lemma, in mathcomp.solvable.nilpotent]
+morphim_lcn [lemma, in mathcomp.solvable.nilpotent]
+morphim_ucn [lemma, in mathcomp.solvable.nilpotent]
+morphim_der [lemma, in mathcomp.solvable.commutator]
+morphim_homg [lemma, in mathcomp.fingroup.morphism]
+morphim_isom [lemma, in mathcomp.fingroup.morphism]
+morphim_ifactm [lemma, in mathcomp.fingroup.morphism]
+morphim_invmE [lemma, in mathcomp.fingroup.morphism]
+morphim_invm [lemma, in mathcomp.fingroup.morphism]
+morphim_factm [lemma, in mathcomp.fingroup.morphism]
+morphim_comp [lemma, in mathcomp.fingroup.morphism]
+morphim_trivm [lemma, in mathcomp.fingroup.morphism]
+morphim_restrm [lemma, in mathcomp.fingroup.morphism]
+morphim_idm [lemma, in mathcomp.fingroup.morphism]
+morphim_injm_eq1 [lemma, in mathcomp.fingroup.morphism]
+morphim_subnormG [lemma, in mathcomp.fingroup.morphism]
+morphim_normG [lemma, in mathcomp.fingroup.morphism]
+morphim_abelian [lemma, in mathcomp.fingroup.morphism]
+morphim_subcent [lemma, in mathcomp.fingroup.morphism]
+morphim_cents [lemma, in mathcomp.fingroup.morphism]
+morphim_cent [lemma, in mathcomp.fingroup.morphism]
+morphim_subcent1 [lemma, in mathcomp.fingroup.morphism]
+morphim_cent1s [lemma, in mathcomp.fingroup.morphism]
+morphim_cent1 [lemma, in mathcomp.fingroup.morphism]
+morphim_normal [lemma, in mathcomp.fingroup.morphism]
+morphim_subnorm [lemma, in mathcomp.fingroup.morphism]
+morphim_norms [lemma, in mathcomp.fingroup.morphism]
+morphim_norm [lemma, in mathcomp.fingroup.morphism]
+morphim_cycle [lemma, in mathcomp.fingroup.morphism]
+morphim_gen [lemma, in mathcomp.fingroup.morphism]
+morphim_inj [lemma, in mathcomp.fingroup.morphism]
+morphim_injG [lemma, in mathcomp.fingroup.morphism]
+morphim_ker [lemma, in mathcomp.fingroup.morphism]
+morphim_groupset [lemma, in mathcomp.fingroup.morphism]
+morphim_class [lemma, in mathcomp.fingroup.morphism]
+morphim_set1 [lemma, in mathcomp.fingroup.morphism]
+morphim_eq0 [lemma, in mathcomp.fingroup.morphism]
+morphim_setIpre [lemma, in mathcomp.fingroup.morphism]
+morphim_sub [lemma, in mathcomp.fingroup.morphism]
+morphim_spec [inductive, in mathcomp.fingroup.morphism]
+morphim_center [lemma, in mathcomp.solvable.center]
+morphim_cyclic [lemma, in mathcomp.solvable.cyclic]
+morphim_Zgroup [lemma, in mathcomp.solvable.sylow]
+Morphim.aT [variable, in mathcomp.solvable.pgroup]
+Morphim.aT [variable, in mathcomp.character.character]
+Morphim.aT [variable, in mathcomp.character.classfun]
+Morphim.D [variable, in mathcomp.solvable.pgroup]
+Morphim.D [variable, in mathcomp.character.character]
+Morphim.D [variable, in mathcomp.character.classfun]
+Morphim.f [variable, in mathcomp.solvable.pgroup]
+Morphim.f [variable, in mathcomp.character.character]
+Morphim.f [variable, in mathcomp.character.classfun]
+Morphim.G [variable, in mathcomp.character.character]
+Morphim.Main [section, in mathcomp.character.classfun]
+Morphim.Main.G [variable, in mathcomp.character.classfun]
+Morphim.Main.sGD [variable, in mathcomp.character.classfun]
+Morphim.rT [variable, in mathcomp.solvable.pgroup]
+Morphim.rT [variable, in mathcomp.character.character]
+Morphim.rT [variable, in mathcomp.character.classfun]
+Morphim.sGD [variable, in mathcomp.character.character]
+morphim0 [lemma, in mathcomp.fingroup.morphism]
+morphim1 [lemma, in mathcomp.fingroup.morphism]
+MorphInduced [section, in mathcomp.character.classfun]
+MorphInduced.aT [variable, in mathcomp.character.classfun]
+MorphInduced.D [variable, in mathcomp.character.classfun]
+MorphInduced.eq_hg [variable, in mathcomp.character.classfun]
+MorphInduced.g [variable, in mathcomp.character.classfun]
+MorphInduced.G [variable, in mathcomp.character.classfun]
+MorphInduced.h [variable, in mathcomp.character.classfun]
+MorphInduced.H [variable, in mathcomp.character.classfun]
+MorphInduced.isoG [variable, in mathcomp.character.classfun]
+MorphInduced.isoH [variable, in mathcomp.character.classfun]
+MorphInduced.R [variable, in mathcomp.character.classfun]
+MorphInduced.rT [variable, in mathcomp.character.classfun]
+MorphInduced.S [variable, in mathcomp.character.classfun]
+MorphInduced.sHG [variable, in mathcomp.character.classfun]
+Morphism [section, in mathcomp.ssreflect.generic_quotient]
+morphism [record, in mathcomp.fingroup.morphism]
+Morphism [constructor, in mathcomp.fingroup.morphism]
+morphism [library]
+MorphismComposition [section, in mathcomp.fingroup.morphism]
+MorphismComposition.f [variable, in mathcomp.fingroup.morphism]
+MorphismComposition.g [variable, in mathcomp.fingroup.morphism]
+MorphismComposition.G [variable, in mathcomp.fingroup.morphism]
+MorphismComposition.gT [variable, in mathcomp.fingroup.morphism]
+MorphismComposition.H [variable, in mathcomp.fingroup.morphism]
+MorphismComposition.hT [variable, in mathcomp.fingroup.morphism]
+MorphismComposition.rT [variable, in mathcomp.fingroup.morphism]
+MorphismOps1 [section, in mathcomp.fingroup.morphism]
+MorphismOps1.aT [variable, in mathcomp.fingroup.morphism]
+MorphismOps1.D [variable, in mathcomp.fingroup.morphism]
+MorphismOps1.f [variable, in mathcomp.fingroup.morphism]
+MorphismOps1.rT [variable, in mathcomp.fingroup.morphism]
+MorphismStructure [section, in mathcomp.fingroup.morphism]
+MorphismStructure.A [variable, in mathcomp.fingroup.morphism]
+MorphismStructure.aT [variable, in mathcomp.fingroup.morphism]
+MorphismStructure.D [variable, in mathcomp.fingroup.morphism]
+MorphismStructure.f [variable, in mathcomp.fingroup.morphism]
+MorphismStructure.R [variable, in mathcomp.fingroup.morphism]
+MorphismStructure.rT [variable, in mathcomp.fingroup.morphism]
+MorphismStructure.x [variable, in mathcomp.fingroup.morphism]
+MorphismStructure.y [variable, in mathcomp.fingroup.morphism]
+MorphismTheory [section, in mathcomp.fingroup.morphism]
+MorphismTheory.aT [variable, in mathcomp.fingroup.morphism]
+MorphismTheory.D [variable, in mathcomp.fingroup.morphism]
+MorphismTheory.f [variable, in mathcomp.fingroup.morphism]
+MorphismTheory.Injective [section, in mathcomp.fingroup.morphism]
+MorphismTheory.Injective.injf [variable, in mathcomp.fingroup.morphism]
+MorphismTheory.rT [variable, in mathcomp.fingroup.morphism]
+morphism_for [definition, in mathcomp.fingroup.morphism]
+Morphism.a [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.b [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.f [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.fq [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.g [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.gq [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.h [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.hq [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.p [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.pi_h [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.pi_r [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.pi_p [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.pi_g [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.pi_f [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.pq [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.qT [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.qU [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.r [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.rq [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.T [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.U [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.x [variable, in mathcomp.ssreflect.generic_quotient]
+Morphism.y [variable, in mathcomp.ssreflect.generic_quotient]
+MorphIsometry [section, in mathcomp.character.classfun]
+MorphIsometry.gT [variable, in mathcomp.character.classfun]
+morphJ [lemma, in mathcomp.fingroup.morphism]
+morphm [definition, in mathcomp.fingroup.morphism]
+morphM [lemma, in mathcomp.fingroup.morphism]
+morphmE [lemma, in mathcomp.fingroup.morphism]
+MorphNil [section, in mathcomp.solvable.nilpotent]
+MorphNil.aT [variable, in mathcomp.solvable.nilpotent]
+MorphNil.D [variable, in mathcomp.solvable.nilpotent]
+MorphNil.f [variable, in mathcomp.solvable.nilpotent]
+MorphNil.rT [variable, in mathcomp.solvable.nilpotent]
+MorphOrder [section, in mathcomp.character.classfun]
+MorphOrder.aT [variable, in mathcomp.character.classfun]
+MorphOrder.f [variable, in mathcomp.character.classfun]
+MorphOrder.G [variable, in mathcomp.character.classfun]
+MorphOrder.R [variable, in mathcomp.character.classfun]
+MorphOrder.rT [variable, in mathcomp.character.classfun]
+MorphPcore [section, in mathcomp.solvable.pgroup]
+MorphPcore.PcoreMod [section, in mathcomp.solvable.pgroup]
+MorphPcore.PcoreMod.F [variable, in mathcomp.solvable.pgroup]
+MorphPoly [section, in mathcomp.algebra.poly]
+MorphPoly.aR [variable, in mathcomp.algebra.poly]
+MorphPoly.pf [variable, in mathcomp.algebra.poly]
+MorphPoly.rR [variable, in mathcomp.algebra.poly]
+morphpre [definition, in mathcomp.fingroup.morphism]
+morphpreD [lemma, in mathcomp.fingroup.morphism]
+morphpreE [lemma, in mathcomp.fingroup.morphism]
+morphpreI [lemma, in mathcomp.fingroup.morphism]
+morphpreIdom [lemma, in mathcomp.fingroup.morphism]
+morphpreIim [lemma, in mathcomp.fingroup.morphism]
+morphpreJ [lemma, in mathcomp.fingroup.morphism]
+morphpreK [lemma, in mathcomp.fingroup.morphism]
+MorphPreMax [section, in mathcomp.solvable.gseries]
+MorphPreMax.D [variable, in mathcomp.solvable.gseries]
+MorphPreMax.dG [variable, in mathcomp.solvable.gseries]
+MorphPreMax.dM [variable, in mathcomp.solvable.gseries]
+MorphPreMax.f [variable, in mathcomp.solvable.gseries]
+MorphPreMax.G [variable, in mathcomp.solvable.gseries]
+MorphPreMax.gT [variable, in mathcomp.solvable.gseries]
+MorphPreMax.M [variable, in mathcomp.solvable.gseries]
+MorphPreMax.rT [variable, in mathcomp.solvable.gseries]
+morphpreMl [lemma, in mathcomp.fingroup.morphism]
+morphpreMr [lemma, in mathcomp.fingroup.morphism]
+morphpreP [lemma, in mathcomp.fingroup.morphism]
+morphpreS [lemma, in mathcomp.fingroup.morphism]
+morphpreSK [lemma, in mathcomp.fingroup.morphism]
+morphpreT [lemma, in mathcomp.fingroup.morphism]
+morphpreU [lemma, in mathcomp.fingroup.morphism]
+morphpreV [lemma, in mathcomp.fingroup.morphism]
+morphpre_qisom [lemma, in mathcomp.fingroup.quotient]
+morphpre_quotm [lemma, in mathcomp.fingroup.quotient]
+morphpre_mx_abs_irr [lemma, in mathcomp.character.mxrepresentation]
+morphpre_mx_irr [lemma, in mathcomp.character.mxrepresentation]
+morphpre_mx_repr [lemma, in mathcomp.character.mxrepresentation]
+morphpre_maximal_eq [lemma, in mathcomp.solvable.gseries]
+morphpre_maximal [lemma, in mathcomp.solvable.gseries]
+morphpre_ifactm [lemma, in mathcomp.fingroup.morphism]
+morphpre_invm [lemma, in mathcomp.fingroup.morphism]
+morphpre_factm [lemma, in mathcomp.fingroup.morphism]
+morphpre_comp [lemma, in mathcomp.fingroup.morphism]
+morphpre_restrm [lemma, in mathcomp.fingroup.morphism]
+morphpre_idm [lemma, in mathcomp.fingroup.morphism]
+morphpre_subcent [lemma, in mathcomp.fingroup.morphism]
+morphpre_cents [lemma, in mathcomp.fingroup.morphism]
+morphpre_cent [lemma, in mathcomp.fingroup.morphism]
+morphpre_subcent1 [lemma, in mathcomp.fingroup.morphism]
+morphpre_cent1s [lemma, in mathcomp.fingroup.morphism]
+morphpre_cent1 [lemma, in mathcomp.fingroup.morphism]
+morphpre_subnorm [lemma, in mathcomp.fingroup.morphism]
+morphpre_normal [lemma, in mathcomp.fingroup.morphism]
+morphpre_norms [lemma, in mathcomp.fingroup.morphism]
+morphpre_norm [lemma, in mathcomp.fingroup.morphism]
+morphpre_gen [lemma, in mathcomp.fingroup.morphism]
+morphpre_inj [lemma, in mathcomp.fingroup.morphism]
+morphpre_proper [lemma, in mathcomp.fingroup.morphism]
+morphpre_set1 [lemma, in mathcomp.fingroup.morphism]
+morphpre_groupset [lemma, in mathcomp.fingroup.morphism]
+morphpre_sub [lemma, in mathcomp.fingroup.morphism]
+morphpre0 [lemma, in mathcomp.fingroup.morphism]
+morphR [lemma, in mathcomp.fingroup.morphism]
+MorphSol [section, in mathcomp.solvable.nilpotent]
+MorphSol.D [variable, in mathcomp.solvable.nilpotent]
+MorphSol.f [variable, in mathcomp.solvable.nilpotent]
+MorphSol.G [variable, in mathcomp.solvable.nilpotent]
+MorphSol.gT [variable, in mathcomp.solvable.nilpotent]
+MorphSol.rT [variable, in mathcomp.solvable.nilpotent]
+MorphSubNormal [section, in mathcomp.solvable.gseries]
+MorphSubNormal.gT [variable, in mathcomp.solvable.gseries]
+MorphTheory [section, in mathcomp.algebra.ssrint]
+MorphTheory.Additive [section, in mathcomp.algebra.ssrint]
+MorphTheory.Additive.f [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Additive.U [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Additive.V [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Frobenius [section, in mathcomp.algebra.ssrint]
+MorphTheory.Frobenius.charFp [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Frobenius.p [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Frobenius.R [variable, in mathcomp.algebra.ssrint]
+_ ^f [notation, in mathcomp.algebra.ssrint]
+MorphTheory.Linear [section, in mathcomp.algebra.ssrint]
+MorphTheory.Linear.f [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Linear.R [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Linear.U [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Linear.V [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Multiplicative [section, in mathcomp.algebra.ssrint]
+MorphTheory.Multiplicative.f [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Multiplicative.R [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Multiplicative.S [variable, in mathcomp.algebra.ssrint]
+MorphTheory.NumMorphism [section, in mathcomp.algebra.ssrint]
+MorphTheory.NumMorphism.PO [section, in mathcomp.algebra.ssrint]
+MorphTheory.NumMorphism.PO.R [variable, in mathcomp.algebra.ssrint]
+MorphTheory.ZintBigMorphism [section, in mathcomp.algebra.ssrint]
+MorphTheory.ZintBigMorphism.R [variable, in mathcomp.algebra.ssrint]
+MorphTheory.Zintmul1rMorph [section, in mathcomp.algebra.ssrint]
+MorphTheory.Zintmul1rMorph.R [variable, in mathcomp.algebra.ssrint]
+morphV [lemma, in mathcomp.fingroup.morphism]
+morphX [lemma, in mathcomp.fingroup.morphism]
+morph_constt [lemma, in mathcomp.solvable.pgroup]
+morph_p_elt [lemma, in mathcomp.solvable.pgroup]
+morph_Iirr_eq0 [lemma, in mathcomp.character.character]
+morph_Iirr_inj [lemma, in mathcomp.character.character]
+morph_IirrE [lemma, in mathcomp.character.character]
+morph_Iirr0 [lemma, in mathcomp.character.character]
+morph_Iirr [definition, in mathcomp.character.character]
+morph_gact_irr [lemma, in mathcomp.fingroup.action]
+morph_gacent [lemma, in mathcomp.fingroup.action]
+morph_gastab [lemma, in mathcomp.fingroup.action]
+morph_gastabs [lemma, in mathcomp.fingroup.action]
+morph_afix [lemma, in mathcomp.fingroup.action]
+morph_astab [lemma, in mathcomp.fingroup.action]
+morph_astabs [lemma, in mathcomp.fingroup.action]
+morph_act [definition, in mathcomp.fingroup.action]
+morph_injm_eq1 [lemma, in mathcomp.fingroup.morphism]
+morph_dom_groupset [lemma, in mathcomp.fingroup.morphism]
+morph_prod [lemma, in mathcomp.fingroup.morphism]
+morph_generator [lemma, in mathcomp.solvable.cyclic]
+morph_order [lemma, in mathcomp.solvable.cyclic]
+morph1 [lemma, in mathcomp.fingroup.morphism]
+MPi [module, in mathcomp.ssreflect.generic_quotient]
+mpiE [lemma, in mathcomp.ssreflect.generic_quotient]
+MPi.E [definition, in mathcomp.ssreflect.generic_quotient]
+MPi.f [definition, in mathcomp.ssreflect.generic_quotient]
+mulfxA [lemma, in mathcomp.field.fieldext]
+mulfxC [lemma, in mathcomp.field.fieldext]
+mulfx_addl [lemma, in mathcomp.field.fieldext]
+mulg [definition, in mathcomp.fingroup.fingroup]
+mulgA [lemma, in mathcomp.fingroup.fingroup]
+mulgI [lemma, in mathcomp.fingroup.fingroup]
+mulGid [lemma, in mathcomp.fingroup.fingroup]
+mulGidPl [lemma, in mathcomp.fingroup.fingroup]
+mulGidPr [lemma, in mathcomp.fingroup.fingroup]
+mulgK [lemma, in mathcomp.fingroup.fingroup]
+mulgKV [lemma, in mathcomp.fingroup.fingroup]
+mulgm [definition, in mathcomp.fingroup.gproduct]
+mulgmP [lemma, in mathcomp.fingroup.gproduct]
+mulgr_action [definition, in mathcomp.fingroup.action]
+mulGS [lemma, in mathcomp.fingroup.fingroup]
+mulgS [lemma, in mathcomp.fingroup.fingroup]
+mulGSgid [lemma, in mathcomp.fingroup.fingroup]
+mulGSid [lemma, in mathcomp.fingroup.fingroup]
+mulgSS [lemma, in mathcomp.fingroup.fingroup]
+mulGsubP [lemma, in mathcomp.fingroup.fingroup]
+mulgT [abbreviation, in mathcomp.fingroup.fingroup]
+mulgT [abbreviation, in mathcomp.fingroup.fingroup]
+mulgU [lemma, in mathcomp.fingroup.fingroup]
+mulgV [lemma, in mathcomp.fingroup.fingroup]
+mulg_normal_maximal [lemma, in mathcomp.solvable.gseries]
+mulg_exp_card_rcosets [lemma, in mathcomp.solvable.finmodule]
+mulg_nil [lemma, in mathcomp.solvable.nilpotent]
+mulG_sub [lemma, in mathcomp.fingroup.fingroup]
+mulG_subG [lemma, in mathcomp.fingroup.fingroup]
+mulG_subr [lemma, in mathcomp.fingroup.fingroup]
+mulG_subl [lemma, in mathcomp.fingroup.fingroup]
+mulg_set1 [lemma, in mathcomp.fingroup.fingroup]
+mulg_subr [lemma, in mathcomp.fingroup.fingroup]
+mulg_subl [lemma, in mathcomp.fingroup.fingroup]
+mulg0 [lemma, in mathcomp.fingroup.gproduct]
+mulg1 [lemma, in mathcomp.fingroup.fingroup]
+mulIg [lemma, in mathcomp.fingroup.fingroup]
+mulKg [lemma, in mathcomp.fingroup.fingroup]
+mulKmx [lemma, in mathcomp.algebra.matrix]
+mulKn [lemma, in mathcomp.ssreflect.div]
+mulKVg [lemma, in mathcomp.fingroup.fingroup]
+mulKVmx [lemma, in mathcomp.algebra.matrix]
+mulKz [lemma, in mathcomp.algebra.intdiv]
+mulmx [definition, in mathcomp.algebra.matrix]
+mulmxA [lemma, in mathcomp.algebra.matrix]
+mulmxBl [lemma, in mathcomp.algebra.matrix]
+mulmxBr [lemma, in mathcomp.algebra.matrix]
+mulmxDl [lemma, in mathcomp.algebra.matrix]
+mulmxDr [lemma, in mathcomp.algebra.matrix]
+mulmxE [lemma, in mathcomp.algebra.matrix]
+mulmxK [lemma, in mathcomp.algebra.matrix]
+mulmxKpV [lemma, in mathcomp.algebra.mxalgebra]
+mulmxKV [lemma, in mathcomp.algebra.matrix]
+mulmxKV_ker [lemma, in mathcomp.algebra.mxalgebra]
+mulmxN [lemma, in mathcomp.algebra.matrix]
+mulmxnE [lemma, in mathcomp.algebra.matrix]
+mulmxr [abbreviation, in mathcomp.algebra.matrix]
+mulmxr [abbreviation, in mathcomp.algebra.matrix]
+mulmxr_is_linear [lemma, in mathcomp.algebra.matrix]
+mulmxr_head [definition, in mathcomp.algebra.matrix]
+mulmxV [lemma, in mathcomp.algebra.matrix]
+mulmx_is_scalable [lemma, in mathcomp.algebra.matrix]
+mulmx_block [lemma, in mathcomp.algebra.matrix]
+mulmx_diag [lemma, in mathcomp.algebra.matrix]
+mulmx_sum_row [lemma, in mathcomp.algebra.matrix]
+mulmx_sumr [lemma, in mathcomp.algebra.matrix]
+mulmx_suml [lemma, in mathcomp.algebra.matrix]
+mulmx_key [lemma, in mathcomp.algebra.matrix]
+mulmx_ker [lemma, in mathcomp.algebra.mxalgebra]
+mulmx_sub [lemma, in mathcomp.algebra.mxalgebra]
+mulmx_coker [lemma, in mathcomp.algebra.mxalgebra]
+mulmx_max_rank [lemma, in mathcomp.algebra.mxalgebra]
+mulmx_base [lemma, in mathcomp.algebra.mxalgebra]
+mulmx_ebase [lemma, in mathcomp.algebra.mxalgebra]
+mulmx0 [lemma, in mathcomp.algebra.matrix]
+mulmx0_rank_max [lemma, in mathcomp.algebra.mxalgebra]
+mulmx1 [lemma, in mathcomp.algebra.matrix]
+mulmx1C [lemma, in mathcomp.algebra.matrix]
+mulmx1_unit [lemma, in mathcomp.algebra.matrix]
+mulmx1_min [lemma, in mathcomp.algebra.matrix]
+mulmx1_min_rank [lemma, in mathcomp.algebra.mxalgebra]
+muln [definition, in mathcomp.ssreflect.ssrnat]
+mulnA [lemma, in mathcomp.ssreflect.ssrnat]
+mulnAC [lemma, in mathcomp.ssreflect.ssrnat]
+mulnACA [lemma, in mathcomp.ssreflect.ssrnat]
+mulnb [lemma, in mathcomp.ssreflect.ssrnat]
+mulnbl [lemma, in mathcomp.ssreflect.ssrnat]
+mulnBl [lemma, in mathcomp.ssreflect.ssrnat]
+mulnbr [lemma, in mathcomp.ssreflect.ssrnat]
+mulnBr [lemma, in mathcomp.ssreflect.ssrnat]
+mulnC [lemma, in mathcomp.ssreflect.ssrnat]
+mulnCA [lemma, in mathcomp.ssreflect.ssrnat]
+mulnDl [lemma, in mathcomp.ssreflect.ssrnat]
+mulnDr [lemma, in mathcomp.ssreflect.ssrnat]
+mulnE [lemma, in mathcomp.ssreflect.ssrnat]
+mulnK [lemma, in mathcomp.ssreflect.div]
+mulNmx [lemma, in mathcomp.algebra.matrix]
+mulnn [lemma, in mathcomp.ssreflect.ssrnat]
+mulNrNz [lemma, in mathcomp.algebra.ssrint]
+mulNrz [lemma, in mathcomp.algebra.ssrint]
+mulnS [lemma, in mathcomp.ssreflect.ssrnat]
+mulnSr [lemma, in mathcomp.ssreflect.ssrnat]
+muln_lcml [lemma, in mathcomp.ssreflect.div]
+muln_lcmr [lemma, in mathcomp.ssreflect.div]
+muln_lcm_gcd [lemma, in mathcomp.ssreflect.div]
+muln_divCA_gcd [lemma, in mathcomp.ssreflect.div]
+muln_gcdl [lemma, in mathcomp.ssreflect.div]
+muln_gcdr [lemma, in mathcomp.ssreflect.div]
+muln_divCA [lemma, in mathcomp.ssreflect.div]
+muln_divA [lemma, in mathcomp.ssreflect.div]
+muln_modl [lemma, in mathcomp.ssreflect.div]
+muln_modr [lemma, in mathcomp.ssreflect.div]
+muln_grepr [definition, in mathcomp.character.character]
+muln_cfunE [lemma, in mathcomp.character.classfun]
+muln_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
+muln_eq1 [lemma, in mathcomp.ssreflect.ssrnat]
+muln_eq0 [lemma, in mathcomp.ssreflect.ssrnat]
+muln_rec [definition, in mathcomp.ssreflect.ssrnat]
+muln0 [lemma, in mathcomp.ssreflect.ssrnat]
+muln1 [lemma, in mathcomp.ssreflect.ssrnat]
+muln2 [lemma, in mathcomp.ssreflect.ssrnat]
+mulpT [definition, in mathcomp.field.closed_field]
+mulpz [lemma, in mathcomp.algebra.ssrint]
+mulq [definition, in mathcomp.algebra.rat]
+mulqA [lemma, in mathcomp.algebra.rat]
+mulqC [lemma, in mathcomp.algebra.rat]
+mulq_addl [lemma, in mathcomp.algebra.rat]
+mulq_frac [lemma, in mathcomp.algebra.rat]
+mulq_subdefC [lemma, in mathcomp.algebra.rat]
+mulq_subdef [definition, in mathcomp.algebra.rat]
+mulrbz [lemma, in mathcomp.algebra.ssrint]
+mulrIz [lemma, in mathcomp.algebra.ssrint]
+mulrNz [lemma, in mathcomp.algebra.ssrint]
+mulrN1z [lemma, in mathcomp.algebra.ssrint]
+mulrzA [lemma, in mathcomp.algebra.ssrint]
+mulrzAC [lemma, in mathcomp.algebra.ssrint]
+mulrzAl [lemma, in mathcomp.algebra.ssrint]
+mulrzAr [lemma, in mathcomp.algebra.ssrint]
+mulrzA_C [lemma, in mathcomp.algebra.ssrint]
+mulrzBl [lemma, in mathcomp.algebra.ssrint]
+mulrzBl_nat [lemma, in mathcomp.algebra.ssrint]
+mulrzBr [lemma, in mathcomp.algebra.ssrint]
+mulrzDl [lemma, in mathcomp.algebra.ssrint]
+mulrzDr [lemma, in mathcomp.algebra.ssrint]
+mulrzl [lemma, in mathcomp.algebra.ssrint]
+mulrzr [lemma, in mathcomp.algebra.ssrint]
+mulrzz [lemma, in mathcomp.algebra.ssrint]
+mulrz_neq0 [lemma, in mathcomp.algebra.ssrint]
+mulrz_eq0 [lemma, in mathcomp.algebra.ssrint]
+mulrz_le0_ge0 [lemma, in mathcomp.algebra.ssrint]
+mulrz_ge0_le0 [lemma, in mathcomp.algebra.ssrint]
+mulrz_le0 [lemma, in mathcomp.algebra.ssrint]
+mulrz_ge0 [lemma, in mathcomp.algebra.ssrint]
+mulrz_int [lemma, in mathcomp.algebra.ssrint]
+mulrz_suml [lemma, in mathcomp.algebra.ssrint]
+mulrz_sumr [lemma, in mathcomp.algebra.ssrint]
+mulrz_nat [lemma, in mathcomp.algebra.ssrint]
+mulr0z [lemma, in mathcomp.algebra.ssrint]
+mulr1z [lemma, in mathcomp.algebra.ssrint]
+mulr2z [lemma, in mathcomp.algebra.ssrint]
+mulSG [lemma, in mathcomp.fingroup.fingroup]
+mulSg [lemma, in mathcomp.fingroup.fingroup]
+mulSgGid [lemma, in mathcomp.fingroup.fingroup]
+mulSGid [lemma, in mathcomp.fingroup.fingroup]
+mulsgP [lemma, in mathcomp.fingroup.fingroup]
+mulsmx [definition, in mathcomp.algebra.mxalgebra]
+mulsmxA [lemma, in mathcomp.algebra.mxalgebra]
+mulsmxP [lemma, in mathcomp.algebra.mxalgebra]
+mulsmxS [lemma, in mathcomp.algebra.mxalgebra]
+mulsmx_addr [lemma, in mathcomp.algebra.mxalgebra]
+mulsmx_addl [lemma, in mathcomp.algebra.mxalgebra]
+mulsmx_subP [lemma, in mathcomp.algebra.mxalgebra]
+mulsmx0 [lemma, in mathcomp.algebra.mxalgebra]
+mulSn [lemma, in mathcomp.ssreflect.ssrnat]
+mulSnr [lemma, in mathcomp.ssreflect.ssrnat]
+muls_eqmx [lemma, in mathcomp.algebra.mxalgebra]
+muls0mx [lemma, in mathcomp.algebra.mxalgebra]
+multE [lemma, in mathcomp.ssreflect.ssrnat]
+multiplicity_XsubC [lemma, in mathcomp.algebra.poly]
+mulUg [lemma, in mathcomp.fingroup.fingroup]
+mulVg [lemma, in mathcomp.fingroup.fingroup]
+mulVmx [lemma, in mathcomp.algebra.matrix]
+mulVq [lemma, in mathcomp.algebra.rat]
+mulzK [lemma, in mathcomp.algebra.intdiv]
+mulz_divCA_gcd [lemma, in mathcomp.algebra.intdiv]
+mulz_gcdl [lemma, in mathcomp.algebra.intdiv]
+mulz_gcdr [lemma, in mathcomp.algebra.intdiv]
+mulz_divCA [lemma, in mathcomp.algebra.intdiv]
+mulz_divA [lemma, in mathcomp.algebra.intdiv]
+mulz_modl [lemma, in mathcomp.algebra.intdiv]
+mulz_modr [lemma, in mathcomp.algebra.intdiv]
+mulz_Nsign_abs [lemma, in mathcomp.algebra.ssrint]
+mulz_sign_abs [lemma, in mathcomp.algebra.ssrint]
+mulz_sg_eqN1 [lemma, in mathcomp.algebra.ssrint]
+mulz_sg_eq1 [lemma, in mathcomp.algebra.ssrint]
+mulz_sg [lemma, in mathcomp.algebra.ssrint]
+mulz2 [lemma, in mathcomp.algebra.ssrint]
+mul_subdefA [lemma, in mathcomp.algebra.rat]
+mul_bin_left [lemma, in mathcomp.ssreflect.binomial]
+mul_bin_down [lemma, in mathcomp.ssreflect.binomial]
+mul_bin_diag [lemma, in mathcomp.ssreflect.binomial]
+mul_vchar [lemma, in mathcomp.character.vcharacter]
+mul_pair [definition, in mathcomp.algebra.ssralg]
+mul_adj_mx [lemma, in mathcomp.algebra.matrix]
+mul_mx_adj [lemma, in mathcomp.algebra.matrix]
+mul_mx_scalar [lemma, in mathcomp.algebra.matrix]
+mul_vec_lin_row [lemma, in mathcomp.algebra.matrix]
+mul_vec_lin [lemma, in mathcomp.algebra.matrix]
+mul_rV_lin [lemma, in mathcomp.algebra.matrix]
+mul_rV_lin1 [lemma, in mathcomp.algebra.matrix]
+mul_block_col [lemma, in mathcomp.algebra.matrix]
+mul_row_block [lemma, in mathcomp.algebra.matrix]
+mul_col_row [lemma, in mathcomp.algebra.matrix]
+mul_row_col [lemma, in mathcomp.algebra.matrix]
+mul_col_mx [lemma, in mathcomp.algebra.matrix]
+mul_mx_row [lemma, in mathcomp.algebra.matrix]
+mul_pid_mx_copid [lemma, in mathcomp.algebra.matrix]
+mul_copid_mx_pid [lemma, in mathcomp.algebra.matrix]
+mul_pid_mx [lemma, in mathcomp.algebra.matrix]
+mul_xcol [lemma, in mathcomp.algebra.matrix]
+mul_row_perm [lemma, in mathcomp.algebra.matrix]
+mul_col_perm [lemma, in mathcomp.algebra.matrix]
+mul_scalar_mx [lemma, in mathcomp.algebra.matrix]
+mul_mx_diag [lemma, in mathcomp.algebra.matrix]
+mul_diag_mx [lemma, in mathcomp.algebra.matrix]
+mul_delta_mx_0 [lemma, in mathcomp.algebra.matrix]
+mul_delta_mx [lemma, in mathcomp.algebra.matrix]
+mul_delta_mx_cond [lemma, in mathcomp.algebra.matrix]
+mul_lin_irr [lemma, in mathcomp.character.character]
+mul_conjC_lin_char [lemma, in mathcomp.character.character]
+mul_char [lemma, in mathcomp.character.character]
+mul_mod_Iirr [definition, in mathcomp.character.inertia]
+mul_Iirr [definition, in mathcomp.character.inertia]
+mul_card_Ohm_Mho_abelian [lemma, in mathcomp.solvable.abelian]
+mul_cfuni_on [lemma, in mathcomp.character.classfun]
+mul_cfuni [lemma, in mathcomp.character.classfun]
+mul_polyC [lemma, in mathcomp.algebra.poly]
+mul_lead_coef [lemma, in mathcomp.algebra.poly]
+mul_polyDr [lemma, in mathcomp.algebra.poly]
+mul_polyDl [lemma, in mathcomp.algebra.poly]
+mul_poly1 [lemma, in mathcomp.algebra.poly]
+mul_1poly [lemma, in mathcomp.algebra.poly]
+mul_polyA [lemma, in mathcomp.algebra.poly]
+mul_poly [definition, in mathcomp.algebra.poly]
+mul_poly_key [lemma, in mathcomp.algebra.poly]
+mul_poly_def [definition, in mathcomp.algebra.poly]
+mul_cardG [lemma, in mathcomp.fingroup.fingroup]
+mul_subG [lemma, in mathcomp.fingroup.fingroup]
+mul0g [lemma, in mathcomp.fingroup.gproduct]
+mul0mx [lemma, in mathcomp.algebra.matrix]
+mul0n [lemma, in mathcomp.ssreflect.ssrnat]
+mul0rz [lemma, in mathcomp.algebra.ssrint]
+mul1fx [lemma, in mathcomp.field.fieldext]
+mul1g [lemma, in mathcomp.fingroup.fingroup]
+mul1mx [lemma, in mathcomp.algebra.matrix]
+mul1n [lemma, in mathcomp.ssreflect.ssrnat]
+mul1q [lemma, in mathcomp.algebra.rat]
+mul2n [lemma, in mathcomp.ssreflect.ssrnat]
+mul2z [lemma, in mathcomp.algebra.ssrint]
+MV [abbreviation, in mathcomp.algebra.matrix]
+mxabelem [library]
+mxalgebra [library]
+mxdirect [abbreviation, in mathcomp.algebra.mxalgebra]
+mxdirect [abbreviation, in mathcomp.algebra.mxalgebra]
+mxdirectE [lemma, in mathcomp.algebra.mxalgebra]
+mxdirectEgeq [lemma, in mathcomp.algebra.mxalgebra]
+mxdirectP [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_sums_center [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_adds_center [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_delta [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_sum_eigenspace [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_sumsE [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_sumsP [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_addsP [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_addsE [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_trivial [lemma, in mathcomp.algebra.mxalgebra]
+mxdirect_def [definition, in mathcomp.algebra.mxalgebra]
+mxE [lemma, in mathcomp.algebra.matrix]
+MxIso [constructor, in mathcomp.character.mxrepresentation]
+mxminpoly [definition, in mathcomp.algebra.mxpoly]
+mxminpoly_map [lemma, in mathcomp.algebra.mxpoly]
+mxminpoly_dvd_char [lemma, in mathcomp.algebra.mxpoly]
+mxminpoly_linear_is_scalar [lemma, in mathcomp.algebra.mxpoly]
+mxminpoly_min [lemma, in mathcomp.algebra.mxpoly]
+mxminpoly_monic [lemma, in mathcomp.algebra.mxpoly]
+mxminpoly_nonconstant [lemma, in mathcomp.algebra.mxpoly]
+mxmodule [definition, in mathcomp.character.mxrepresentation]
+mxmoduleP [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_map [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_form_qf [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_form [definition, in mathcomp.character.mxrepresentation]
+mxmodule_quo [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_conj [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_morphim [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_morphpre [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_eqg [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_subg [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_envelop [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_eigenvector [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_trans [lemma, in mathcomp.character.mxrepresentation]
+mxmodule_abelem_subg [lemma, in mathcomp.character.mxabelem]
+mxmodule_abelemG [lemma, in mathcomp.character.mxabelem]
+mxmodule_abelem [lemma, in mathcomp.character.mxabelem]
+mxmodule0 [lemma, in mathcomp.character.mxrepresentation]
+mxmodule1 [lemma, in mathcomp.character.mxrepresentation]
+mxnonsimple [definition, in mathcomp.character.mxrepresentation]
+mxnonsimpleP [lemma, in mathcomp.character.mxrepresentation]
+mxnonsimple_sat [definition, in mathcomp.character.mxrepresentation]
+mxnonsimple_form [definition, in mathcomp.character.mxrepresentation]
+mxpoly [library]
+mxrank [definition, in mathcomp.algebra.mxalgebra]
+mxrankE [lemma, in mathcomp.algebra.mxalgebra]
+mxrankMfree [lemma, in mathcomp.algebra.mxalgebra]
+mxrankM_maxr [lemma, in mathcomp.algebra.mxalgebra]
+mxrankM_maxl [lemma, in mathcomp.algebra.mxalgebra]
+mxrankS [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_rsim [lemma, in mathcomp.character.mxrepresentation]
+mxrank_iso [lemma, in mathcomp.character.mxrepresentation]
+mxrank_in_factmod [lemma, in mathcomp.character.mxrepresentation]
+mxrank_in_submod [lemma, in mathcomp.character.mxrepresentation]
+mxrank_rowg [lemma, in mathcomp.character.mxabelem]
+mxrank_map [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_sum_leqif [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_adds_leqif [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_sum_cap [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_cap_compl [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_disjoint_sum [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_injP [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_mul_ker [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_mul_min [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_Frobenius [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_coker [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_ker [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_compl [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_leqif_eq [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_leqif_sup [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_gen [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_delta [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_unit [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_eq0 [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_opp [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_scale_nz [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_scale [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_add [lemma, in mathcomp.algebra.mxalgebra]
+mxrank_tr [lemma, in mathcomp.algebra.mxalgebra]
+mxrank0 [lemma, in mathcomp.algebra.mxalgebra]
+mxrank1 [lemma, in mathcomp.algebra.mxalgebra]
+MxRepresentation [constructor, in mathcomp.character.mxrepresentation]
+mxrepresentation [library]
+MxReprSim [constructor, in mathcomp.character.mxrepresentation]
+mxring [definition, in mathcomp.algebra.mxalgebra]
+mxring_id_uniq [lemma, in mathcomp.algebra.mxalgebra]
+mxring_idP [lemma, in mathcomp.algebra.mxalgebra]
+mxring_id [definition, in mathcomp.algebra.mxalgebra]
+MxSemisimple [constructor, in mathcomp.character.mxrepresentation]
+mxsemisimple [inductive, in mathcomp.character.mxrepresentation]
+mxsemisimpleS [lemma, in mathcomp.character.mxrepresentation]
+mxsemisimple_reducible [lemma, in mathcomp.character.mxrepresentation]
+mxsemisimple_module [lemma, in mathcomp.character.mxrepresentation]
+mxsemisimple0 [lemma, in mathcomp.character.mxrepresentation]
+mxsimple [definition, in mathcomp.character.mxrepresentation]
+mxsimpleP [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_map [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_abelian_linear [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_morphim [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_eqg [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_subg [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_semisimple [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_iso_simple [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_isoP [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_iso [definition, in mathcomp.character.mxrepresentation]
+mxsimple_cyclic [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_exists [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_module [lemma, in mathcomp.character.mxrepresentation]
+mxsimple_abelem_subg [lemma, in mathcomp.character.mxabelem]
+mxsimple_abelemGP [lemma, in mathcomp.character.mxabelem]
+mxsimple_abelemP [lemma, in mathcomp.character.mxabelem]
+MxSplits [constructor, in mathcomp.character.mxrepresentation]
+mxsplits [inductive, in mathcomp.character.mxrepresentation]
+Mxsum [constructor, in mathcomp.algebra.mxalgebra]
+mxsum_rank [projection, in mathcomp.algebra.mxalgebra]
+mxsum_val [projection, in mathcomp.algebra.mxalgebra]
+mxsum_expr [record, in mathcomp.algebra.mxalgebra]
+mxsum_spec [inductive, in mathcomp.algebra.mxalgebra]
+mxtrace [definition, in mathcomp.algebra.matrix]
+mxtraceD [lemma, in mathcomp.algebra.matrix]
+mxtraceZ [lemma, in mathcomp.algebra.matrix]
+mxtrace_regular [lemma, in mathcomp.character.mxrepresentation]
+mxtrace_Socle [lemma, in mathcomp.character.mxrepresentation]
+mxtrace_component [lemma, in mathcomp.character.mxrepresentation]
+mxtrace_dsum_mod [lemma, in mathcomp.character.mxrepresentation]
+mxtrace_dadd_mod [lemma, in mathcomp.character.mxrepresentation]
+mxtrace_submod1 [lemma, in mathcomp.character.mxrepresentation]
+mxtrace_rsim [lemma, in mathcomp.character.mxrepresentation]
+mxtrace_sub_fact_mod [lemma, in mathcomp.character.mxrepresentation]
+mxtrace_mulC [lemma, in mathcomp.algebra.matrix]
+mxtrace_block [lemma, in mathcomp.algebra.matrix]
+mxtrace_scalar [lemma, in mathcomp.algebra.matrix]
+mxtrace_diag [lemma, in mathcomp.algebra.matrix]
+mxtrace_is_scalar [lemma, in mathcomp.algebra.matrix]
+mxtrace_tr [lemma, in mathcomp.algebra.matrix]
+mxtrace_prod [lemma, in mathcomp.character.character]
+mxtrace0 [lemma, in mathcomp.algebra.matrix]
+mxtrace1 [lemma, in mathcomp.algebra.matrix]
+mxvec [definition, in mathcomp.algebra.matrix]
+mxvecE [lemma, in mathcomp.algebra.matrix]
+mxvecK [lemma, in mathcomp.algebra.matrix]
+mxvec_dotmul [lemma, in mathcomp.algebra.matrix]
+mxvec_delta [lemma, in mathcomp.algebra.matrix]
+mxvec_is_linear [definition, in mathcomp.algebra.matrix]
+mxvec_eq0 [lemma, in mathcomp.algebra.matrix]
+mxvec_indexP [lemma, in mathcomp.algebra.matrix]
+mxvec_index [definition, in mathcomp.algebra.matrix]
+mxvec_cast [lemma, in mathcomp.algebra.matrix]
+mx_irr_gring_op_center_scalar [lemma, in mathcomp.character.integral_char]
+mx_rsim_map [lemma, in mathcomp.character.mxrepresentation]
+mx_irr_map [lemma, in mathcomp.character.mxrepresentation]
+mx_JordanHolder_max [lemma, in mathcomp.character.mxrepresentation]
+mx_JordanHolder [lemma, in mathcomp.character.mxrepresentation]
+mx_JordanHolder_exists [lemma, in mathcomp.character.mxrepresentation]
+mx_butterfly [lemma, in mathcomp.character.mxrepresentation]
+mx_second_rsim [lemma, in mathcomp.character.mxrepresentation]
+mx_Schreier [lemma, in mathcomp.character.mxrepresentation]
+mx_series_rcons [lemma, in mathcomp.character.mxrepresentation]
+mx_series_repr_irr [lemma, in mathcomp.character.mxrepresentation]
+mx_series_lt [lemma, in mathcomp.character.mxrepresentation]
+mx_subseries_module' [lemma, in mathcomp.character.mxrepresentation]
+mx_subseries_module [lemma, in mathcomp.character.mxrepresentation]
+mx_series [abbreviation, in mathcomp.character.mxrepresentation]
+mx_composition_series [definition, in mathcomp.character.mxrepresentation]
+mx_subseries [definition, in mathcomp.character.mxrepresentation]
+mx_factmod_sub [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_in_submod [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_scalar [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_factmod [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_faithful [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_abs_irr [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_irr [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_iso [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_def [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_trans [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_sym [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim_refl [lemma, in mathcomp.character.mxrepresentation]
+mx_rsim [inductive, in mathcomp.character.mxrepresentation]
+mx_irr_abelian_linear [lemma, in mathcomp.character.mxrepresentation]
+mx_faithful_irr_abelian_cyclic [lemma, in mathcomp.character.mxrepresentation]
+mx_faithful_irr_center_cyclic [lemma, in mathcomp.character.mxrepresentation]
+mx_Jacobson_density [lemma, in mathcomp.character.mxrepresentation]
+mx_abs_irrW [lemma, in mathcomp.character.mxrepresentation]
+mx_abs_irr_cent_scalar [lemma, in mathcomp.character.mxrepresentation]
+mx_abs_irrP [lemma, in mathcomp.character.mxrepresentation]
+mx_absolutely_irreducible [definition, in mathcomp.character.mxrepresentation]
+mx_Schur [lemma, in mathcomp.character.mxrepresentation]
+mx_irrP [lemma, in mathcomp.character.mxrepresentation]
+mx_irreducible [definition, in mathcomp.character.mxrepresentation]
+mx_iso_component [lemma, in mathcomp.character.mxrepresentation]
+mx_reducible_semisimple [lemma, in mathcomp.character.mxrepresentation]
+mx_Maschke [lemma, in mathcomp.character.mxrepresentation]
+mx_reducibleS [lemma, in mathcomp.character.mxrepresentation]
+mx_completely_reducible [definition, in mathcomp.character.mxrepresentation]
+mx_Schur_iso [lemma, in mathcomp.character.mxrepresentation]
+mx_Schur_inj_iso [lemma, in mathcomp.character.mxrepresentation]
+mx_Schur_inj [lemma, in mathcomp.character.mxrepresentation]
+mx_Schur_onto [lemma, in mathcomp.character.mxrepresentation]
+mx_iso_simple [lemma, in mathcomp.character.mxrepresentation]
+mx_iso_module [lemma, in mathcomp.character.mxrepresentation]
+mx_iso_trans [lemma, in mathcomp.character.mxrepresentation]
+mx_iso_sym [lemma, in mathcomp.character.mxrepresentation]
+mx_iso_refl [lemma, in mathcomp.character.mxrepresentation]
+mx_iso [inductive, in mathcomp.character.mxrepresentation]
+mx_faithful_inj [lemma, in mathcomp.character.mxrepresentation]
+mx_faithful [definition, in mathcomp.character.mxrepresentation]
+mx_representation [record, in mathcomp.character.mxrepresentation]
+mx_repr [definition, in mathcomp.character.mxrepresentation]
+mx_vec_lin [lemma, in mathcomp.algebra.matrix]
+mx_rV_lin [lemma, in mathcomp.algebra.matrix]
+mx_val [definition, in mathcomp.algebra.matrix]
+mx_root_minpoly [lemma, in mathcomp.algebra.mxpoly]
+mx_inv_hornerK [lemma, in mathcomp.algebra.mxpoly]
+mx_inv_horner0 [lemma, in mathcomp.algebra.mxpoly]
+mx_inv_horner [definition, in mathcomp.algebra.mxpoly]
+mx_poly_ring_isom [lemma, in mathcomp.algebra.mxpoly]
+mx_rsim_standard [lemma, in mathcomp.character.character]
+mx_rsim_socle [lemma, in mathcomp.character.character]
+mx_rsim_dsum [lemma, in mathcomp.character.character]
+mx_rsim_dadd [lemma, in mathcomp.character.character]
+mx_repr0 [lemma, in mathcomp.character.character]
+mx_repr_of_repr [projection, in mathcomp.character.character]
+mx_Fp_stable [lemma, in mathcomp.character.mxabelem]
+mx_Fp_abelem [lemma, in mathcomp.character.mxabelem]
+mx_group_homocyclic [lemma, in mathcomp.character.mxabelem]
+mx_repr_action_faithful [lemma, in mathcomp.character.mxabelem]
+mx_repr_is_groupAction [lemma, in mathcomp.character.mxabelem]
+mx_repr_is_action [lemma, in mathcomp.character.mxabelem]
+mx_repr_actE [lemma, in mathcomp.character.mxabelem]
+mx_repr_act [definition, in mathcomp.character.mxabelem]
+mx_ideal [definition, in mathcomp.algebra.mxalgebra]
+mx'_cast [lemma, in mathcomp.algebra.matrix]
+mx0_is_scalar [lemma, in mathcomp.algebra.matrix]
+mx1_sum_delta [lemma, in mathcomp.algebra.matrix]
+mx11_scalar [lemma, in mathcomp.algebra.matrix]
+
| 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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +