| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 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.p [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_mx_companion [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_allpairs [lemma, in mathcomp.ssreflect.seq]
-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.m [variable, in mathcomp.character.mxrepresentation]
-MatrixGenField.GenField.Bijection2 [section, in mathcomp.character.mxrepresentation]
-MatrixGenField.GenField.Bijection2.m [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.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.nA [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_permutations [lemma, in mathcomp.ssreflect.seq]
-mem_allpairs [lemma, in mathcomp.ssreflect.seq]
-mem_allpairs_dep [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_uniqF [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_nseq [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]
-MonoHomoTheory [section, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.aR [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.aRE [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.aR_anti [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.aR_refl [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.aR' [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.aR'E [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.aT [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.D [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.f [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.InDom [section, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.InDom.aR_anti [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.InDom.D [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.InDom.DifferentDom [section, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.InDom.DifferentDom.D' [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.InDom.rR_anti [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.rR [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.rRE [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.rR_anti [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.rR_refl [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.rR' [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.rR'E [variable, in mathcomp.ssreflect.eqtype]
-MonoHomoTheory.rT [variable, in mathcomp.ssreflect.eqtype]
-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]
-Monotonicity [section, in mathcomp.ssreflect.path]
-Monotonicity [section, in mathcomp.ssreflect.ssrnat]
-Monotonicity.NatToNat [section, in mathcomp.ssreflect.ssrnat]
-Monotonicity.NatToNat.anti_geq [variable, in mathcomp.ssreflect.ssrnat]
-Monotonicity.NatToNat.anti_leq [variable, in mathcomp.ssreflect.ssrnat]
-Monotonicity.NatToNat.D [variable, in mathcomp.ssreflect.ssrnat]
-Monotonicity.NatToNat.D' [variable, in mathcomp.ssreflect.ssrnat]
-Monotonicity.NatToNat.f [variable, in mathcomp.ssreflect.ssrnat]
-Monotonicity.NatToNat.gtn_neqAge [variable, in mathcomp.ssreflect.ssrnat]
-Monotonicity.NatToNat.leq_total [variable, in mathcomp.ssreflect.ssrnat]
-Monotonicity.NatToNat.ltn_neqAle [variable, in mathcomp.ssreflect.ssrnat]
-Monotonicity.r [variable, in mathcomp.ssreflect.path]
-Monotonicity.r_refl [variable, in mathcomp.ssreflect.path]
-Monotonicity.r_trans [variable, in mathcomp.ssreflect.path]
-Monotonicity.T [variable, in mathcomp.ssreflect.path]
-Monotonicity.T [variable, in mathcomp.ssreflect.ssrnat]
-mono_leqif [lemma, in mathcomp.ssreflect.ssrnat]
-mono_inj [lemma, in mathcomp.ssreflect.eqtype]
-mono_inj_in [lemma, in mathcomp.ssreflect.eqtype]
-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_delta_companion [lemma, in mathcomp.algebra.mxpoly]
-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]
-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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -