Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (14626 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (165 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (112 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7292 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (250 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (390 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (84 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3144 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (126 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2221 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (53 entries)

M

m [definition, in extremal]
m [definition, in extremal]
m [definition, in extremal]
m [definition, in extremal]
m [definition, in finmodule]
mact [definition, in action]
mactE [lemma, in action]
mact_is_action [lemma, in action]
MakeAut [section, in automorphism]
MakeAut.f [variable, in automorphism]
MakeAut.G [variable, in automorphism]
MakeAut.Gf [variable, in automorphism]
MakeAut.gT [variable, in automorphism]
MakeAut.injf [variable, in automorphism]
MakeEqTypePred [module, in eqtype]
MakeGroupSetBaseGroup [module, in fingroup]
MakeSeq [section, in seq]
MakeSeq.T [variable, in seq]
MakeSeq.x0 [variable, in seq]
map [definition, in seq]
Map [section, in seq]
MapComp [section, in seq]
MapComp.T1 [variable, in seq]
MapComp.T2 [variable, in seq]
MapComp.T3 [variable, in seq]
MapComRing [section, in mxpoly]
MapComRing.A [variable, in mxpoly]
MapComRing.aR [variable, in mxpoly]
MapComRing.f [variable, in mxpoly]
MapComRing.n' [variable, in mxpoly]
MapComRing.rR [variable, in mxpoly]
MapEqPath [section, in path]
MapEqPath.e [variable, in path]
MapEqPath.e' [variable, in path]
MapEqPath.h [variable, in path]
MapEqPath.Hh [variable, in path]
MapEqPath.T [variable, in path]
MapEqPath.T' [variable, in path]
MapField [section, in mxpoly]
MapFieldMatrix [section, in matrix]
MapFieldMatrix.aF [variable, in matrix]
MapFieldMatrix.f [variable, in matrix]
MapFieldMatrix.rF [variable, in matrix]
MapFieldPoly [section, in poly]
MapFieldPoly.f [variable, in poly]
MapFieldPoly.F [variable, in poly]
MapFieldPoly.R [variable, in poly]
MapField.A [variable, in mxpoly]
MapField.aF [variable, in mxpoly]
MapField.f [variable, in mxpoly]
MapField.n' [variable, in mxpoly]
MapField.rF [variable, in mxpoly]
mapK [lemma, in seq]
MapMatrix [section, in matrix]
MapMatrixSpaces [section, in mxalgebra]
MapMatrixSpaces.aF [variable, in mxalgebra]
MapMatrixSpaces.f [variable, in mxalgebra]
MapMatrixSpaces.rF [variable, in mxalgebra]
MapMatrix.aT [variable, in matrix]
MapMatrix.Block [section, in matrix]
MapMatrix.Block.Adl [variable, in matrix]
MapMatrix.Block.Adr [variable, in matrix]
MapMatrix.Block.Aul [variable, in matrix]
MapMatrix.Block.Aur [variable, in matrix]
MapMatrix.Block.B [variable, in matrix]
MapMatrix.Block.Bh [variable, in matrix]
MapMatrix.Block.Bv [variable, in matrix]
MapMatrix.Block.m1 [variable, in matrix]
MapMatrix.Block.m2 [variable, in matrix]
MapMatrix.Block.n1 [variable, in matrix]
MapMatrix.Block.n2 [variable, in matrix]
MapMatrix.f [variable, in matrix]
MapMatrix.OneMatrix [section, in matrix]
MapMatrix.OneMatrix.A [variable, in matrix]
MapMatrix.OneMatrix.m [variable, in matrix]
MapMatrix.OneMatrix.n [variable, in matrix]
MapMatrix.rT [variable, in matrix]
mapP [lemma, in seq]
MapPath [section, in path]
MapPath.e [variable, in path]
MapPath.e' [variable, in path]
MapPath.h [variable, in path]
MapPath.T [variable, in path]
MapPath.T' [variable, in path]
MapPoly [section, in poly]
MapPolyRoots [section, in poly]
MapPolyRoots.f [variable, in poly]
MapPolyRoots.F [variable, in poly]
MapPolyRoots.R [variable, in poly]
MapPoly.Additive [section, in poly]
MapPoly.Additive.f [variable, in poly]
MapPoly.aR [variable, in poly]
MapPoly.cfu [variable, in poly]
MapPoly.Definitions [section, in poly]
MapPoly.Definitions.f [variable, in poly]
MapPoly.f [variable, in poly]
MapPoly.rR [variable, in poly]
MapPoly.u [variable, in poly]
MapRing [section, in mxpoly]
MapRingMatrix [section, in matrix]
MapRingMatrix.aR [variable, in matrix]
MapRingMatrix.f [variable, in matrix]
MapRingMatrix.FixedSize [section, in matrix]
MapRingMatrix.FixedSize.m [variable, in matrix]
MapRingMatrix.FixedSize.n [variable, in matrix]
MapRingMatrix.FixedSize.p [variable, in matrix]
MapRingMatrix.rR [variable, in matrix]
MapRing.A [variable, in mxpoly]
MapRing.aR [variable, in mxpoly]
MapRing.d [variable, in mxpoly]
MapRing.f [variable, in mxpoly]
MapRing.n [variable, in mxpoly]
MapRing.rR [variable, in mxpoly]
MapZmodMatrix [section, in matrix]
MapZmodMatrix.aR [variable, in matrix]
MapZmodMatrix.f [variable, in matrix]
MapZmodMatrix.m [variable, in matrix]
MapZmodMatrix.n [variable, in matrix]
MapZmodMatrix.rR [variable, in matrix]
map_regular_mx [lemma, in mxrepresentation]
map_cent_mx [lemma, in mxalgebra]
map_unitmx [lemma, in matrix]
map_cat [lemma, in seq]
map_polyE [lemma, in poly]
map_horner_mx [lemma, in mxpoly]
map_row_perm [lemma, in matrix]
map_poly_eq0 [lemma, in poly]
map_col' [lemma, in matrix]
map_mx_inv [lemma, in matrix]
map_ltmx [lemma, in mxalgebra]
map_usubmx [lemma, in matrix]
map_mx_is_multiplicative [lemma, in matrix]
map_mx_sum [definition, in matrix]
map_row' [lemma, in matrix]
map_section_repr [lemma, in mxrepresentation]
map_col_ebase [lemma, in mxalgebra]
map_tuple [definition, in tuple]
map_poly_inj [lemma, in poly]
map_drsubmx [lemma, in matrix]
map_poly_rmorphism [definition, in poly]
map_poly_additive [definition, in poly]
map_diffmx [lemma, in mxalgebra]
map_nseq [lemma, in seq]
map_conform_mx [lemma, in matrix]
map_capmx_gen [definition, in mxalgebra]
map_polyX [lemma, in poly]
map_col_perm [lemma, in matrix]
map_col_mx [lemma, in matrix]
map_tupleE [definition, in vector]
map_poly_is_additive [lemma, in poly]
map_mxD [lemma, in matrix]
map_scalar_mx [lemma, in matrix]
map_const_mx [lemma, in matrix]
map_id_in [lemma, in seq]
map_rcons [lemma, in seq]
map_dlsubmx [lemma, in matrix]
map_repr [definition, in mxrepresentation]
map_mx_inj [lemma, in matrix]
map_trmx [lemma, in matrix]
map_xrow [lemma, in matrix]
map_dsubmx [lemma, in matrix]
map_mx_unit [lemma, in matrix]
map_uniq_roots [lemma, in poly]
map_tnth_enum [lemma, in tuple]
map_id [lemma, in seq]
map_mx_is_scalar [lemma, in matrix]
map_tupleP [lemma, in tuple]
map_complmx [lemma, in mxalgebra]
map_repr_mx [definition, in mxrepresentation]
map_row_ebase [lemma, in mxalgebra]
map_mx0 [lemma, in matrix]
map_row [lemma, in matrix]
map_tperm_mx [lemma, in matrix]
map_mxN [lemma, in matrix]
map_mx [definition, in matrix]
map_lin1_mx [lemma, in matrix]
map_comp [lemma, in seq]
map_ursubmx [lemma, in matrix]
map_vec_mx [lemma, in matrix]
map_row_mx [lemma, in matrix]
map_poly [definition, in poly]
map_mx_eq0 [lemma, in matrix]
map_rot [lemma, in seq]
map_pid_mx [lemma, in matrix]
map_capmx [lemma, in mxalgebra]
map_mulsmx [lemma, in mxalgebra]
map_drop [lemma, in seq]
map_pK [lemma, in seq]
map_inj_in_uniq [lemma, in seq]
map_reprJ [lemma, in mxrepresentation]
map_regular_subseries [lemma, in mxrepresentation]
map_com_poly [lemma, in poly]
map_cons [lemma, in seq]
map_poly_com [lemma, in poly]
map_pinvmx [lemma, in mxalgebra]
map_perm_mx [lemma, in matrix]
map_field_poly_monic [lemma, in poly]
map_eigenspace [lemma, in mxalgebra]
map_rotr [lemma, in seq]
map_preim [lemma, in fintype]
map_char_poly [lemma, in mxpoly]
map_mx_abs_irr [lemma, in mxrepresentation]
map_take [lemma, in seq]
map_mx_sub [lemma, in matrix]
map_mx_adj [lemma, in matrix]
map_ulsubmx [lemma, in matrix]
map_genmx [lemma, in mxalgebra]
map_rfix_mx [lemma, in mxrepresentation]
map_addsmx [lemma, in mxalgebra]
map_mxvec [lemma, in matrix]
map_mx1 [lemma, in matrix]
map_copid_mx [lemma, in matrix]
map_lsubmx [lemma, in matrix]
map_uniq [lemma, in seq]
map_castmx [lemma, in matrix]
map_eqmx [lemma, in mxalgebra]
map_diff_roots [lemma, in poly]
map_gring_row [lemma, in mxrepresentation]
map_poly_scaler [lemma, in poly]
map_kermx [lemma, in mxalgebra]
map_submx [lemma, in mxalgebra]
map_col_base [lemma, in mxalgebra]
map_gring_proj [lemma, in mxrepresentation]
map_mxZ [lemma, in matrix]
map_com_coef [lemma, in poly]
map_modp [lemma, in poly]
map_polyXn [lemma, in poly]
map_col [lemma, in matrix]
map_delta_mx [lemma, in matrix]
map_diag_mx [lemma, in matrix]
map_mx_rmorphism [definition, in matrix]
map_mx_additive [definition, in matrix]
map_char_poly_mx [lemma, in mxpoly]
map_f [lemma, in seq]
map_mx_repr [lemma, in mxrepresentation]
map_ffun_enum [lemma, in finfun]
map_enveloping_algebra_mx [lemma, in mxrepresentation]
map_cokermx [lemma, in mxalgebra]
map_group_ring [lemma, in mxrepresentation]
map_divp [lemma, in poly]
map_invmx [lemma, in matrix]
map_regular_repr [lemma, in mxrepresentation]
map_mask [lemma, in seq]
map_polyC [lemma, in poly]
map_powers_mx [lemma, in mxpoly]
map_rsubmx [lemma, in matrix]
map_row_base [lemma, in mxalgebra]
map_gring_op [lemma, in mxrepresentation]
map_poly_rV [lemma, in mxpoly]
map_mx_inv_horner [lemma, in mxpoly]
map_mx_faithful [lemma, in mxrepresentation]
map_inj_uniq [lemma, in seq]
map_lin_mx [lemma, in matrix]
map_rev [lemma, in seq]
map_mxM [lemma, in matrix]
map_xcol [lemma, in matrix]
map_rVpoly [lemma, in mxpoly]
map_block_mx [lemma, in matrix]
map_subseq [lemma, in seq]
map_center_mx [lemma, in mxalgebra]
map_gring_mx [lemma, in mxrepresentation]
map_reprE [lemma, in mxrepresentation]
map_poly_is_rmorphism [lemma, in poly]
Map.f [variable, in seq]
Map.Hf [variable, in seq]
Map.n0 [variable, in seq]
Map.T1 [variable, in seq]
Map.T2 [variable, in seq]
Map.x1 [variable, in seq]
Map.x2 [variable, in seq]
Mask [section, in seq]
mask [definition, in seq]
mask_cons [lemma, in seq]
mask_uniq [lemma, in seq]
mask_false [lemma, in seq]
mask_rot [lemma, in seq]
mask_true [lemma, in seq]
mask_cat [lemma, in seq]
Mask.n0 [variable, in seq]
Mask.T [variable, in seq]
mask0 [lemma, in seq]
mask1 [lemma, in seq]
master_key [lemma, in ssreflect]
matrix [inductive, in matrix]
Matrix [constructor, in matrix]
matrix [library]
MatrixAlgebra [section, in matrix]
MatrixAlgebra [section, in mxalgebra]
MatrixAlgebra.CentMxDef [section, in mxalgebra]
MatrixAlgebra.CentMxDef.m [variable, in mxalgebra]
MatrixAlgebra.CentMxDef.n [variable, in mxalgebra]
MatrixAlgebra.CentMxDef.R [variable, in mxalgebra]
MatrixAlgebra.F [variable, in mxalgebra]
MatrixAlgebra.LiftPerm [section, in matrix]
MatrixAlgebra.LiftPerm.n [variable, in matrix]
MatrixAlgebra.LinMatrix [section, in matrix]
MatrixAlgebra.LinMatrix.f [variable, in matrix]
MatrixAlgebra.LinMatrix.m1 [variable, in matrix]
MatrixAlgebra.LinMatrix.m2 [variable, in matrix]
MatrixAlgebra.LinMatrix.n1 [variable, in matrix]
MatrixAlgebra.LinMatrix.n2 [variable, in matrix]
MatrixAlgebra.LinRowVector [section, in matrix]
MatrixAlgebra.LinRowVector.f [variable, in matrix]
MatrixAlgebra.LinRowVector.m [variable, in matrix]
MatrixAlgebra.LinRowVector.n [variable, in matrix]
MatrixAlgebra.MatrixRing [section, in matrix]
MatrixAlgebra.MatrixRing.n' [variable, in matrix]
MatrixAlgebra.Mulmxr [section, in matrix]
MatrixAlgebra.Mulmxr.m [variable, in matrix]
MatrixAlgebra.Mulmxr.n [variable, in matrix]
MatrixAlgebra.Mulmxr.p [variable, in matrix]
MatrixAlgebra.R [variable, in matrix]
MatrixAlgebra.RingModule [section, in matrix]
MatrixAlgebra.RingModule.m [variable, in matrix]
MatrixAlgebra.RingModule.n [variable, in matrix]
MatrixAlgebra.ScalarMx [section, in matrix]
MatrixAlgebra.ScalarMx.n [variable, in matrix]
MatrixAlgebra.StructuralLinear [section, in matrix]
MatrixAlgebra.Trace [section, in matrix]
MatrixAlgebra.Trace.n [variable, in matrix]
MatrixDef [section, in matrix]
MatrixDef.m [variable, in matrix]
MatrixDef.n [variable, in matrix]
MatrixDef.R [variable, in matrix]
MatrixFormula [module, in mxpoly]
MatrixFormula.Add [abbreviation, in mxpoly]
MatrixFormula.And [abbreviation, in mxpoly]
MatrixFormula.Bool [abbreviation, in mxpoly]
MatrixFormula.eval [abbreviation, in mxpoly]
MatrixFormula.eval_vec_mx [lemma, in mxpoly]
MatrixFormula.eval_mxvec [lemma, in mxpoly]
MatrixFormula.eval_row_var [lemma, in mxpoly]
MatrixFormula.eval_col_mx [lemma, in mxpoly]
MatrixFormula.eval_submx [lemma, in mxpoly]
MatrixFormula.eval_mx_term [lemma, in mxpoly]
MatrixFormula.eval_mxrank [lemma, in mxpoly]
MatrixFormula.eval_mx [definition, in mxpoly]
MatrixFormula.eval_mulmx [lemma, in mxpoly]
MatrixFormula.Exists_rowP [lemma, in mxpoly]
MatrixFormula.Exists_row_form [definition, in mxpoly]
MatrixFormula.False [abbreviation, in mxpoly]
MatrixFormula.form [abbreviation, in mxpoly]
MatrixFormula.holds [abbreviation, in mxpoly]
MatrixFormula.MatrixFormula [section, in mxpoly]
MatrixFormula.MatrixFormula.Env [section, in mxpoly]
MatrixFormula.MatrixFormula.Env.d [variable, in mxpoly]
MatrixFormula.MatrixFormula.F [variable, in mxpoly]
MatrixFormula.MatrixFormula.Subsetmx [section, in mxpoly]
MatrixFormula.MatrixFormula.Subsetmx.A [variable, in mxpoly]
MatrixFormula.MatrixFormula.Subsetmx.B [variable, in mxpoly]
MatrixFormula.MatrixFormula.Subsetmx.m1 [variable, in mxpoly]
MatrixFormula.MatrixFormula.Subsetmx.m2 [variable, in mxpoly]
MatrixFormula.MatrixFormula.Subsetmx.n [variable, in mxpoly]
MatrixFormula.morphAnd [abbreviation, in mxpoly]
MatrixFormula.mulmx_term [definition, in mxpoly]
MatrixFormula.mxrank_form_qf [lemma, in mxpoly]
MatrixFormula.mxrank_form [definition, in mxpoly]
MatrixFormula.mx_term [definition, in mxpoly]
MatrixFormula.nth_seq_of_rV [lemma, in mxpoly]
MatrixFormula.nth_row_env [lemma, in mxpoly]
MatrixFormula.qf_form [abbreviation, in mxpoly]
MatrixFormula.qf_eval [abbreviation, in mxpoly]
MatrixFormula.row_var [definition, in mxpoly]
MatrixFormula.row_env [definition, in mxpoly]
MatrixFormula.Schur [definition, in mxpoly]
MatrixFormula.seq_of_rV [definition, in mxpoly]
MatrixFormula.size_seq_of_rV [lemma, in mxpoly]
MatrixFormula.submx_form_qf [lemma, in mxpoly]
MatrixFormula.submx_form [definition, in mxpoly]
MatrixFormula.term [abbreviation, in mxpoly]
MatrixFormula.True [abbreviation, in mxpoly]
MatrixGenField [module, in mxrepresentation]
MatrixGenField.Ad [abbreviation, in mxrepresentation]
MatrixGenField.Ad [abbreviation, in mxrepresentation]
MatrixGenField.Ad'T [definition, in mxrepresentation]
MatrixGenField.base [definition, in mxrepresentation]
MatrixGenField.base_full [lemma, in mxrepresentation]
MatrixGenField.base_free [lemma, in mxrepresentation]
MatrixGenField.Bool [abbreviation, in mxrepresentation]
MatrixGenField.card_gen [lemma, in mxrepresentation]
MatrixGenField.d [abbreviation, in mxrepresentation]
MatrixGenField.d [abbreviation, in mxrepresentation]
MatrixGenField.DecideGenField [section, in mxrepresentation]
MatrixGenField.DecideGenField.A [variable, in mxrepresentation]
MatrixGenField.DecideGenField.cGA [variable, in mxrepresentation]
MatrixGenField.DecideGenField.F [variable, in mxrepresentation]
MatrixGenField.DecideGenField.G [variable, in mxrepresentation]
MatrixGenField.DecideGenField.gT [variable, in mxrepresentation]
MatrixGenField.DecideGenField.irrG [variable, in mxrepresentation]
MatrixGenField.DecideGenField.n' [variable, in mxrepresentation]
MatrixGenField.DecideGenField.rG [variable, in mxrepresentation]
MatrixGenField.d_gt0 [definition, in mxrepresentation]
MatrixGenField.d_gt0 [definition, in mxrepresentation]
MatrixGenField.eval_mulT [lemma, in mxrepresentation]
MatrixGenField.eval_gen_term [lemma, in mxrepresentation]
MatrixGenField.eval_mxT [definition, in mxrepresentation]
MatrixGenField.FA [abbreviation, in mxrepresentation]
MatrixGenField.FA [abbreviation, in mxrepresentation]
MatrixGenField.FA [abbreviation, in mxrepresentation]
MatrixGenField.False [abbreviation, in mxrepresentation]
MatrixGenField.FiniteGenField [section, in mxrepresentation]
MatrixGenField.FiniteGenField.A [variable, in mxrepresentation]
MatrixGenField.FiniteGenField.cGA [variable, in mxrepresentation]
MatrixGenField.FiniteGenField.F [variable, in mxrepresentation]
MatrixGenField.FiniteGenField.G [variable, in mxrepresentation]
MatrixGenField.FiniteGenField.gT [variable, in mxrepresentation]
MatrixGenField.FiniteGenField.irrG [variable, in mxrepresentation]
MatrixGenField.FiniteGenField.n' [variable, in mxrepresentation]
MatrixGenField.FiniteGenField.rG [variable, in mxrepresentation]
MatrixGenField.form [abbreviation, in mxrepresentation]
MatrixGenField.Gen [constructor, in mxrepresentation]
MatrixGenField.gen [definition, in mxrepresentation]
MatrixGenField.genD [definition, in mxrepresentation]
MatrixGenField.GenField [section, in mxrepresentation]
MatrixGenField.GenField.A [variable, in mxrepresentation]
MatrixGenField.GenField.Bijection [section, in mxrepresentation]
MatrixGenField.GenField.Bijection.m1 [variable, in mxrepresentation]
MatrixGenField.GenField.Bijection2 [section, in mxrepresentation]
MatrixGenField.GenField.Bijection2.m1 [variable, in mxrepresentation]
MatrixGenField.GenField.cGA [variable, in mxrepresentation]
MatrixGenField.GenField.F [variable, in mxrepresentation]
MatrixGenField.GenField.G [variable, in mxrepresentation]
MatrixGenField.GenField.gT [variable, in mxrepresentation]
MatrixGenField.GenField.irrG [variable, in mxrepresentation]
MatrixGenField.GenField.n' [variable, in mxrepresentation]
MatrixGenField.GenField.rG [variable, in mxrepresentation]
MatrixGenField.genK [lemma, in mxrepresentation]
MatrixGenField.genM [definition, in mxrepresentation]
MatrixGenField.genN [definition, in mxrepresentation]
MatrixGenField.genV [definition, in mxrepresentation]
MatrixGenField.gen_is_rmorphism [lemma, in mxrepresentation]
MatrixGenField.gen_dim_factor [lemma, in mxrepresentation]
MatrixGenField.gen_env [definition, in mxrepresentation]
MatrixGenField.gen_addA [lemma, in mxrepresentation]
MatrixGenField.gen_mulDr [lemma, in mxrepresentation]
MatrixGenField.gen_mx_faithful [lemma, in mxrepresentation]
MatrixGenField.gen_mulC [lemma, in mxrepresentation]
MatrixGenField.gen_finFieldType [definition, in mxrepresentation]
MatrixGenField.gen_finIdomainType [definition, in mxrepresentation]
MatrixGenField.gen_finComUnitRingType [definition, in mxrepresentation]
MatrixGenField.gen_finUnitRingType [definition, in mxrepresentation]
MatrixGenField.gen_finComRingType [definition, in mxrepresentation]
MatrixGenField.gen_finRingType [definition, in mxrepresentation]
MatrixGenField.gen_finGroupType [definition, in mxrepresentation]
MatrixGenField.gen_baseFinGroupType [definition, in mxrepresentation]
MatrixGenField.gen_finZmodType [definition, in mxrepresentation]
MatrixGenField.gen_subFinType [definition, in mxrepresentation]
MatrixGenField.gen_finType [definition, in mxrepresentation]
MatrixGenField.gen_subCountType [definition, in mxrepresentation]
MatrixGenField.gen_countType [definition, in mxrepresentation]
MatrixGenField.gen_decFieldType [definition, in mxrepresentation]
MatrixGenField.gen_repr [definition, in mxrepresentation]
MatrixGenField.gen_rmorphism [definition, in mxrepresentation]
MatrixGenField.gen_additive [definition, in mxrepresentation]
MatrixGenField.gen_fieldType [definition, in mxrepresentation]
MatrixGenField.gen_idomainType [definition, in mxrepresentation]
MatrixGenField.gen_comUnitRingType [definition, in mxrepresentation]
MatrixGenField.gen_unitRingType [definition, in mxrepresentation]
MatrixGenField.gen_comRingType [definition, in mxrepresentation]
MatrixGenField.gen_ringType [definition, in mxrepresentation]
MatrixGenField.gen_zmodType [definition, in mxrepresentation]
MatrixGenField.gen_choiceType [definition, in mxrepresentation]
MatrixGenField.gen_eqType [definition, in mxrepresentation]
MatrixGenField.gen_subType [definition, in mxrepresentation]
MatrixGenField.gen_base [definition, in mxrepresentation]
MatrixGenField.gen_form [definition, in mxrepresentation]
MatrixGenField.gen_finMixin [definition, in mxrepresentation]
MatrixGenField.gen_dim_gt0 [lemma, in mxrepresentation]
MatrixGenField.gen_of [record, in mxrepresentation]
MatrixGenField.gen_choiceMixin [definition, in mxrepresentation]
MatrixGenField.gen_ringMixin [definition, in mxrepresentation]
MatrixGenField.gen_fieldMixin [definition, in mxrepresentation]
MatrixGenField.gen_mulA [lemma, in mxrepresentation]
MatrixGenField.gen_mx_irr [lemma, in mxrepresentation]
MatrixGenField.gen_dim [definition, in mxrepresentation]
MatrixGenField.gen_ntriv [lemma, in mxrepresentation]
MatrixGenField.gen_idomainMixin [definition, in mxrepresentation]
MatrixGenField.gen_term [definition, in mxrepresentation]
MatrixGenField.gen_mx_repr [lemma, in mxrepresentation]
MatrixGenField.gen_addC [lemma, in mxrepresentation]
MatrixGenField.gen_invr0 [lemma, in mxrepresentation]
MatrixGenField.gen_dim_ex_proof [lemma, in mxrepresentation]
MatrixGenField.gen_mx [definition, in mxrepresentation]
MatrixGenField.gen_sat [definition, in mxrepresentation]
MatrixGenField.gen_countMixin [definition, in mxrepresentation]
MatrixGenField.gen_unitRingMixin [definition, in mxrepresentation]
MatrixGenField.gen_add0r [lemma, in mxrepresentation]
MatrixGenField.gen_decFieldMixin [definition, in mxrepresentation]
MatrixGenField.gen_satP [lemma, in mxrepresentation]
MatrixGenField.gen_mulVr [lemma, in mxrepresentation]
MatrixGenField.gen_eqMixin [definition, in mxrepresentation]
MatrixGenField.gen_zmodMixin [definition, in mxrepresentation]
MatrixGenField.gen_dim_ub_proof [lemma, in mxrepresentation]
MatrixGenField.gen_addNr [lemma, in mxrepresentation]
MatrixGenField.gen_mul1r [lemma, in mxrepresentation]
MatrixGenField.gen0 [definition, in mxrepresentation]
MatrixGenField.gen1 [definition, in mxrepresentation]
MatrixGenField.groot [definition, in mxrepresentation]
MatrixGenField.inFA [abbreviation, in mxrepresentation]
MatrixGenField.inFA [definition, in mxrepresentation]
MatrixGenField.in_genD [lemma, in mxrepresentation]
MatrixGenField.in_genK [lemma, in mxrepresentation]
MatrixGenField.in_gen_row [lemma, in mxrepresentation]
MatrixGenField.in_gen_sum [definition, in mxrepresentation]
MatrixGenField.in_gen0 [lemma, in mxrepresentation]
MatrixGenField.in_genZ [lemma, in mxrepresentation]
MatrixGenField.in_genJ [lemma, in mxrepresentation]
MatrixGenField.in_gen [definition, in mxrepresentation]
MatrixGenField.in_genN [lemma, in mxrepresentation]
MatrixGenField.irr [abbreviation, in mxrepresentation]
MatrixGenField.m [abbreviation, in mxrepresentation]
MatrixGenField.map_mxminpoly_groot [lemma, in mxrepresentation]
MatrixGenField.morphAnd [abbreviation, in mxrepresentation]
MatrixGenField.mulT [definition, in mxrepresentation]
MatrixGenField.mxmodule_rowval_gen [lemma, in mxrepresentation]
MatrixGenField.mxT [definition, in mxrepresentation]
MatrixGenField.mxval [definition, in mxrepresentation]
MatrixGenField.mxvalD [lemma, in mxrepresentation]
MatrixGenField.mxvalM [lemma, in mxrepresentation]
MatrixGenField.mxvalN [lemma, in mxrepresentation]
MatrixGenField.mxvalV [lemma, in mxrepresentation]
MatrixGenField.mxval_gen1 [lemma, in mxrepresentation]
MatrixGenField.mxval_rmorphism [definition, in mxrepresentation]
MatrixGenField.mxval_additive [definition, in mxrepresentation]
MatrixGenField.mxval_centg [lemma, in mxrepresentation]
MatrixGenField.mxval_is_multiplicative [lemma, in mxrepresentation]
MatrixGenField.mxval_inj [lemma, in mxrepresentation]
MatrixGenField.mxval_grootX [lemma, in mxrepresentation]
MatrixGenField.mxval_groot [lemma, in mxrepresentation]
MatrixGenField.mxval_sub [lemma, in mxrepresentation]
MatrixGenField.mxval_genM [lemma, in mxrepresentation]
MatrixGenField.mxval_genV [lemma, in mxrepresentation]
MatrixGenField.mxval_sum [definition, in mxrepresentation]
MatrixGenField.mxval0 [lemma, in mxrepresentation]
MatrixGenField.mxval1 [lemma, in mxrepresentation]
MatrixGenField.n [abbreviation, in mxrepresentation]
MatrixGenField.n [abbreviation, in mxrepresentation]
MatrixGenField.n [abbreviation, in mxrepresentation]
MatrixGenField.non_linear_gen_reducible [lemma, in mxrepresentation]
MatrixGenField.nth_map_rVval [lemma, in mxrepresentation]
MatrixGenField.pA [abbreviation, in mxrepresentation]
MatrixGenField.pval [definition, in mxrepresentation]
MatrixGenField.rfix_gen [lemma, in mxrepresentation]
MatrixGenField.rGA [abbreviation, in mxrepresentation]
MatrixGenField.rker_gen [lemma, in mxrepresentation]
MatrixGenField.rowval_genK [lemma, in mxrepresentation]
MatrixGenField.rowval_gen [definition, in mxrepresentation]
MatrixGenField.rowval_gen_stable [lemma, in mxrepresentation]
MatrixGenField.row_gen_sum_mxval [lemma, in mxrepresentation]
MatrixGenField.rstabs_rowval_gen [lemma, in mxrepresentation]
MatrixGenField.rstabs_in_gen [lemma, in mxrepresentation]
MatrixGenField.rstab_in_gen [lemma, in mxrepresentation]
MatrixGenField.rVval [projection, in mxrepresentation]
MatrixGenField.sat_gen_form [lemma, in mxrepresentation]
MatrixGenField.set_nth_map_rVval [lemma, in mxrepresentation]
MatrixGenField.subbase [definition, in mxrepresentation]
MatrixGenField.submx_rowval_gen [lemma, in mxrepresentation]
MatrixGenField.submx_in_gen [lemma, in mxrepresentation]
MatrixGenField.submx_in_gen_eq [lemma, in mxrepresentation]
MatrixGenField.term [abbreviation, in mxrepresentation]
MatrixGenField.True [abbreviation, in mxrepresentation]
MatrixGenField.val_genK [lemma, in mxrepresentation]
MatrixGenField.val_gen0 [lemma, in mxrepresentation]
MatrixGenField.val_genJ [lemma, in mxrepresentation]
MatrixGenField.val_genZ [lemma, in mxrepresentation]
MatrixGenField.val_gen_sum [definition, in mxrepresentation]
MatrixGenField.val_gen_row [lemma, in mxrepresentation]
MatrixGenField.val_genJmx [definition, in mxrepresentation]
MatrixGenField.val_genN [lemma, in mxrepresentation]
MatrixGenField.val_gen_rV [lemma, in mxrepresentation]
MatrixGenField.val_genD [lemma, in mxrepresentation]
MatrixGenField.val_gen [definition, in mxrepresentation]
MatrixInv [section, in matrix]
MatrixInv.Defs [section, in matrix]
MatrixInv.Defs.n [variable, in matrix]
MatrixInv.n' [variable, in matrix]
MatrixInv.R [variable, in matrix]
matrixP [lemma, in matrix]
MatrixStructural [section, in matrix]
MatrixStructural.Block [section, in matrix]
MatrixStructural.Block.CatBlock [section, in matrix]
MatrixStructural.Block.CatBlock.Adl [variable, in matrix]
MatrixStructural.Block.CatBlock.Adr [variable, in matrix]
MatrixStructural.Block.CatBlock.Aul [variable, in matrix]
MatrixStructural.Block.CatBlock.Aur [variable, in matrix]
MatrixStructural.Block.CutBlock [section, in matrix]
MatrixStructural.Block.CutBlock.A [variable, in matrix]
MatrixStructural.Block.m1 [variable, in matrix]
MatrixStructural.Block.m2 [variable, in matrix]
MatrixStructural.Block.n1 [variable, in matrix]
MatrixStructural.Block.n2 [variable, in matrix]
MatrixStructural.CutPaste [section, in matrix]
MatrixStructural.CutPaste.m [variable, in matrix]
MatrixStructural.CutPaste.m1 [variable, in matrix]
MatrixStructural.CutPaste.m2 [variable, in matrix]
MatrixStructural.CutPaste.n [variable, in matrix]
MatrixStructural.CutPaste.n1 [variable, in matrix]
MatrixStructural.CutPaste.n2 [variable, in matrix]
MatrixStructural.FixedDim [section, in matrix]
MatrixStructural.FixedDim.m [variable, in matrix]
MatrixStructural.FixedDim.n [variable, in matrix]
MatrixStructural.R [variable, in matrix]
MatrixStructural.TrBlock [section, in matrix]
MatrixStructural.TrBlock.Adl [variable, in matrix]
MatrixStructural.TrBlock.Adr [variable, in matrix]
MatrixStructural.TrBlock.Aul [variable, in matrix]
MatrixStructural.TrBlock.Aur [variable, in matrix]
MatrixStructural.TrBlock.m1 [variable, in matrix]
MatrixStructural.TrBlock.m2 [variable, in matrix]
MatrixStructural.TrBlock.n1 [variable, in matrix]
MatrixStructural.TrBlock.n2 [variable, in matrix]
MatrixStructural.TrCutBlock [section, in matrix]
MatrixStructural.TrCutBlock.A [variable, in matrix]
MatrixStructural.TrCutBlock.m1 [variable, in matrix]
MatrixStructural.TrCutBlock.m2 [variable, in matrix]
MatrixStructural.TrCutBlock.n1 [variable, in matrix]
MatrixStructural.TrCutBlock.n2 [variable, in matrix]
MatrixStructural.VecMatrix [section, in matrix]
MatrixStructural.VecMatrix.m [variable, in matrix]
MatrixStructural.VecMatrix.n [variable, in matrix]
matrixVectMixin [definition, in vector]
matrixVectType [definition, in vector]
MatrixZmodule [section, in matrix]
MatrixZmodule.Additive [section, in matrix]
MatrixZmodule.Additive.f [variable, in matrix]
MatrixZmodule.Additive.g [variable, in matrix]
MatrixZmodule.Additive.m [variable, in matrix]
MatrixZmodule.Additive.n [variable, in matrix]
MatrixZmodule.Additive.p [variable, in matrix]
MatrixZmodule.Additive.q [variable, in matrix]
MatrixZmodule.FixedDim [section, in matrix]
MatrixZmodule.FixedDim.m [variable, in matrix]
MatrixZmodule.FixedDim.n [variable, in matrix]
MatrixZmodule.V [variable, in matrix]
matrix_countMixin [definition, in matrix]
matrix_modr [lemma, in mxalgebra]
matrix_ringMixin [definition, in matrix]
matrix_nonzero1 [lemma, in matrix]
matrix_lmodMixin [definition, in matrix]
matrix_finMixin [definition, in matrix]
matrix_zmodMixin [definition, in matrix]
matrix_of_fun [definition, in matrix]
matrix_eqMixin [definition, in matrix]
matrix_modl [lemma, in mxalgebra]
matrix_finUnitRingType [definition, in matrix]
matrix_unitAlg [definition, in matrix]
matrix_unitRing [definition, in matrix]
matrix_algType [definition, in matrix]
matrix_finRingType [definition, in matrix]
matrix_lAlgType [definition, in matrix]
matrix_ringType [definition, in matrix]
matrix_lmodType [definition, in matrix]
matrix_finGroupType [definition, in matrix]
matrix_baseFinGroupType [definition, in matrix]
matrix_finZmodType [definition, in matrix]
matrix_zmodType [definition, in matrix]
matrix_subFinType [definition, in matrix]
matrix_finType [definition, in matrix]
matrix_subCountType [definition, in matrix]
matrix_countType [definition, in matrix]
matrix_choiceType [definition, in matrix]
matrix_eqType [definition, in matrix]
matrix_subType [definition, in matrix]
matrix_unitRingMixin [definition, in matrix]
matrix_sum_delta [lemma, in matrix]
matrix_choiceMixin [definition, in matrix]
maxainv [definition, in jordanholder]
maxainvM [lemma, in jordanholder]
maxainvS [lemma, in jordanholder]
maxainv_norm [lemma, in jordanholder]
maxainv_exists [lemma, in jordanholder]
maxainv_sub [lemma, in jordanholder]
maxainv_asimple_quo [lemma, in jordanholder]
maxainv_ainvar [lemma, in jordanholder]
maxainv_proper [lemma, in jordanholder]
maxgroup [definition, in fingroup]
maxgroupP [lemma, in fingroup]
maxgroupp [lemma, in fingroup]
maxgroup_exists [lemma, in fingroup]
maximal [definition, in gseries]
maximal [library]
maximalJ [lemma, in gseries]
maximal_cycle_extremal [lemma, in extremal]
maximal_exists [lemma, in gseries]
maximal_eq [definition, in gseries]
maximal_eqP [lemma, in gseries]
maximal_eqJ [lemma, in gseries]
maxKn [lemma, in ssrnat]
maxminset [lemma, in finset]
maxn [definition, in ssrnat]
maxnA [lemma, in ssrnat]
maxnAC [lemma, in ssrnat]
maxnC [lemma, in ssrnat]
maxnCA [lemma, in ssrnat]
maxnK [lemma, in ssrnat]
maxnl [lemma, in ssrnat]
maxnn [lemma, in ssrnat]
maxnormal [definition, in gseries]
maxnormalM [lemma, in gseries]
MaxNormalProps [section, in gseries]
MaxNormalProps.gT [variable, in gseries]
maxnormal_normal [lemma, in gseries]
maxnormal_sub [lemma, in gseries]
maxnormal_proper [lemma, in gseries]
maxnormal_charsimple [lemma, in maximal]
maxnr [lemma, in ssrnat]
maxn_minl [lemma, in ssrnat]
maxn_mulr [lemma, in ssrnat]
maxn_mull [lemma, in ssrnat]
maxn_addoid [definition, in bigop]
maxn_comoid [definition, in bigop]
maxn_monoid [definition, in bigop]
maxn_minr [lemma, in ssrnat]
maxn0 [lemma, in ssrnat]
MaxProps [section, in gseries]
MaxProps.gT [variable, in gseries]
MaxRoots [section, in poly]
MaxRoots.R [variable, in poly]
maxset [definition, in finset]
MaxSetMinSet [section, in finset]
MaxSetMinSet.T [variable, in finset]
maxsetp [lemma, in finset]
maxsetP [lemma, in finset]
maxsetsup [lemma, in finset]
maxset_exists [lemma, in finset]
maxset_eq [lemma, in finset]
max_pdiv_dvd [lemma, in prime]
max_size_mx_series [lemma, in mxrepresentation]
max_pdiv_leq [lemma, in prime]
max_submodP [lemma, in mxrepresentation]
max_unity_roots [lemma, in poly]
max_pgroupJ [lemma, in pgroup]
max_poly_roots [lemma, in poly]
max_card [lemma, in fintype]
max_pdiv_max [lemma, in prime]
max_ring_poly_roots [lemma, in poly]
max_submod [definition, in mxrepresentation]
max_pdiv [definition, in prime]
max_SCN [lemma, in maximal]
max_submod_eqmx [lemma, in mxrepresentation]
max_pdiv_gt0 [lemma, in prime]
max_pgroup_Sylow [lemma, in sylow]
max_pdiv_prime [lemma, in prime]
max0n [lemma, in ssrnat]
meet_center_nil [lemma, in nilpotent]
meet_Ohm1 [lemma, in abelian]
Mem [constructor, in ssrbool]
mem [definition, in ssrbool]
memE [definition, in ssrbool]
memJ_conjg [lemma, in fingroup]
memJ_norm [lemma, in fingroup]
memJ_class [lemma, in fingroup]
memmx_subP [lemma, in mxalgebra]
memmx_eqP [lemma, in mxalgebra]
memmx_map [lemma, in mxalgebra]
memmx_cent_envelop [lemma, in mxrepresentation]
memmx_sumsP [lemma, in mxalgebra]
memmx_addsP [lemma, in mxalgebra]
memmx0 [lemma, in mxalgebra]
memmx1 [lemma, in mxalgebra]
memPredType [definition, in ssrbool]
memtE [lemma, in tuple]
memvD [lemma, in vector]
memvDl [lemma, in vector]
memvDr [lemma, in vector]
memvf [lemma, in vector]
memvMn [lemma, in vector]
memvN [lemma, in vector]
memvNl [lemma, in vector]
memvNr [lemma, in vector]
memvZ [lemma, in vector]
memvZl [lemma, in vector]
memv_pick [lemma, in vector]
memv_sub [lemma, in vector]
memv_inj [lemma, in vector]
memv_subl [lemma, in vector]
memV_rcosetV [lemma, in fingroup]
memv_basis [lemma, in vector]
memv_pi2 [lemma, in vector]
memv_addP [lemma, in vector]
memv_is_basis [lemma, in vector]
memV_lcosetV [lemma, in fingroup]
memv_ker [lemma, in vector]
memv_suml [lemma, in vector]
memv_sumr [lemma, in vector]
memv_imgP [lemma, in vector]
memv_projC [lemma, in vector]
memv_pre_img [lemma, in vector]
memv_sum_pi [lemma, in vector]
memv_is_span [lemma, in vector]
memv_add [lemma, in vector]
memv_span [lemma, in vector]
memV_invg [lemma, in fingroup]
memv_cap [lemma, in vector]
memv_img [lemma, in vector]
memv_sumP [lemma, in vector]
memv_pi1 [lemma, in vector]
memv_proj [lemma, in vector]
memv_subr [lemma, in vector]
memv0 [lemma, in vector]
mem_nth [lemma, in seq]
mem_dprod [lemma, in gproduct]
mem_Hall_pcore [lemma, in pgroup]
mem_cat [lemma, in seq]
mem_undup [lemma, in seq]
mem_remgr [lemma, in gproduct]
mem_setact [lemma, in action]
mem_sdprod [lemma, in gproduct]
mem_seq4 [lemma, in seq]
mem_head [lemma, in seq]
mem_commg [lemma, in fingroup]
mem_morphpre [lemma, in morphism]
mem_conjg [lemma, in fingroup]
mem_filter [lemma, in seq]
mem_iinv [lemma, in fintype]
mem_lcosets [lemma, in fingroup]
mem_classes [lemma, in fingroup]
mem_mask_cons [lemma, in seq]
mem_prev [lemma, in path]
mem_index_iota [lemma, in bigop]
mem_sub_gring [lemma, in mxrepresentation]
mem_p_elt [lemma, in pgroup]
mem_rot [lemma, in seq]
mem_invg [lemma, in fingroup]
mem_conjgV [lemma, in fingroup]
mem_rotr [lemma, in seq]
mem_mulsmx [lemma, in mxalgebra]
mem_rcons [lemma, in seq]
mem_enum [lemma, in fintype]
mem_quotient [lemma, in quotient]
mem_orbit [lemma, in action]
mem_subseq [lemma, in seq]
mem_pmap [lemma, in seq]
mem_imset [lemma, in finset]
mem_morphim [lemma, in morphism]
mem_unity_roots [lemma, in poly]
mem_sum_enum [lemma, in fintype]
mem_image [lemma, in fintype]
mem_pcycle [lemma, in perm]
mem_primes [lemma, in prime]
mem_seq_sub_enum [lemma, in fintype]
mem_pred [inductive, in ssrbool]
mem_repr_rcoset [lemma, in fingroup]
mem_imset2 [lemma, in finset]
mem_topred [lemma, in ssrbool]
mem_gen [lemma, in fingroup]
mem_lcoset [lemma, in fingroup]
mem_mem [lemma, in ssrbool]
mem_prime_decomp [lemma, in prime]
mem_gring_mx [lemma, in mxrepresentation]
mem_cycle [lemma, in fingroup]
mem_simpl [lemma, in ssrbool]
mem_rcosets [lemma, in fingroup]
mem_rcoset [lemma, in fingroup]
mem_take [lemma, in seq]
mem_repr_coset [lemma, in quotient]
mem_sort [lemma, in path]
mem_last [lemma, in seq]
mem_iota [lemma, in seq]
mem_pmap_sub [lemma, in seq]
mem_mask [lemma, in seq]
mem_rev [lemma, in seq]
mem_normal_Hall [lemma, in pgroup]
mem_behead [lemma, in seq]
mem_cover_at [lemma, in finset]
mem_sub_enum [lemma, in fintype]
mem_rowg [lemma, in mxabelem]
mem_bigdprod [lemma, in gproduct]
mem_im_abelem_rV [lemma, in mxabelem]
mem_merge [lemma, in path]
mem_seq [definition, in seq]
mem_ord_enum [lemma, in fintype]
mem_seq_predType [definition, in seq]
mem_belast [lemma, in seq]
mem_allpairs [lemma, in seq]
mem_mask_rot [lemma, in seq]
mem_map [lemma, in seq]
mem_next [lemma, in path]
mem_seq1 [lemma, in seq]
mem_drop [lemma, in seq]
mem_mulg [lemma, in fingroup]
mem_seq3 [lemma, in seq]
mem_seq2 [lemma, in seq]
mem_rVabelem [lemma, in mxabelem]
mem_repr [lemma, in fingroup]
mem_prodg [lemma, in fingroup]
mem_divgr [lemma, in gproduct]
mem0mx [lemma, in mxalgebra]
mem0v [lemma, in vector]
mem2 [definition, in path]
mem2l [lemma, in path]
mem2lf [lemma, in path]
mem2lr_splice [lemma, in path]
mem2l_cat [lemma, in path]
mem2r [lemma, in path]
mem2rf [lemma, in path]
mem2r_cat [lemma, in path]
mem2_cons [lemma, in path]
mem2_cat [lemma, in path]
mem2_map [lemma, in path]
mem2_splice [lemma, in path]
mem2_splice1 [lemma, in path]
mem2_last [lemma, in path]
merge [definition, in path]
merge_sort_rec [definition, in path]
merge_sort_push [definition, in path]
merge_sort_pop [definition, in path]
merge_uniq [lemma, in path]
Metacyclic [section, in cyclic]
metacyclic [definition, in cyclic]
metacyclicN [lemma, in cyclic]
metacyclicP [lemma, in cyclic]
Metacyclic.gT [variable, in cyclic]
metacyclic1 [lemma, in cyclic]
mfun [projection, in morphism]
mG [abbreviation, in mxrepresentation]
mgFunc_id [definition, in gfunctor]
Mho [definition, in abelian]
MhoE [lemma, in abelian]
MhoEabelian [lemma, in abelian]
MhoJ [lemma, in abelian]
MhoS [lemma, in abelian]
Mho_mgFun [definition, in abelian]
Mho_gFun [definition, in abelian]
Mho_igFun [definition, in abelian]
Mho_group [definition, in abelian]
Mho_dprod [lemma, in abelian]
Mho_normal [lemma, in abelian]
Mho_leq [lemma, in abelian]
Mho_sub [lemma, in abelian]
Mho_p_cycle [lemma, in abelian]
Mho_char [lemma, in abelian]
Mho_p_elt [lemma, in abelian]
Mho_cprod [lemma, in abelian]
Mho_cont [lemma, in abelian]
Mho0 [lemma, in abelian]
Mho1 [lemma, in abelian]
mingroup [definition, in fingroup]
mingroupP [lemma, in fingroup]
mingroupp [lemma, in fingroup]
mingroup_exists [lemma, in fingroup]
minKn [lemma, in ssrnat]
MinMaxGroup [section, in fingroup]
MinMaxGroup.G [variable, in fingroup]
MinMaxGroup.gP [variable, in fingroup]
MinMaxGroup.gPG [variable, in fingroup]
MinMaxGroup.gT [variable, in fingroup]
minmaxset [lemma, in finset]
minn [definition, in ssrnat]
minnA [lemma, in ssrnat]
minnAC [lemma, in ssrnat]
minnC [lemma, in ssrnat]
minnCA [lemma, in ssrnat]
minnK [lemma, in ssrnat]
minnl [lemma, in ssrnat]
minnn [lemma, in ssrnat]
minnormal [definition, in gseries]
minnormal_solvable [lemma, in maximal]
minnormal_charsimple [lemma, in maximal]
minnormal_exists [lemma, in gseries]
minnr [lemma, in ssrnat]
minn_to_maxn [lemma, in ssrnat]
minn_mulr [lemma, in ssrnat]
minn_mull [lemma, in ssrnat]
minn_maxr [lemma, in ssrnat]
minn_maxl [lemma, in ssrnat]
minn0 [lemma, in ssrnat]
MinPoly [section, in mxpoly]
minpoly_mxM [lemma, in mxpoly]
minpoly_mx_free [lemma, in mxpoly]
minpoly_mx1 [lemma, in mxpoly]
minpoly_mx_ring [lemma, in mxpoly]
MinPoly.A [variable, in mxpoly]
MinPoly.F [variable, in mxpoly]
MinPoly.n' [variable, in mxpoly]
MinProps [section, in gseries]
MinProps.gT [variable, in gseries]
minset [definition, in finset]
minsetinf [lemma, in finset]
minsetp [lemma, in finset]
minsetP [lemma, in finset]
minset_exists [lemma, in finset]
minset_eq [lemma, in finset]
minusE [lemma, in ssrnat]
min_card_extraspecial [lemma, in maximal]
min0n [lemma, in ssrnat]
misom [definition, in morphism]
misomP [lemma, in morphism]
misom_isog [lemma, in morphism]
mker [lemma, in morphism]
mkerl [lemma, in morphism]
mkerr [lemma, in morphism]
mkfactors [definition, in jordanholder]
mkPredType [definition, in ssrbool]
mkSec [definition, in jordanholder]
mkseq [definition, in seq]
mkseq_uniq [lemma, in seq]
mkseq_nth [lemma, in seq]
mksrepr [definition, in jordanholder]
Mmn [abbreviation, in mxabelem]
modact [definition, in action]
modactE [lemma, in action]
modactEcond [lemma, in action]
ModAction [section, in action]
ModAction.aT [variable, in action]
ModAction.D [variable, in action]
ModAction.GenericMod [section, in action]
ModAction.GenericMod.H [variable, in action]
ModAction.GenericMod.Stabilizers [section, in action]
ModAction.GenericMod.Stabilizers.cSH [variable, in action]
ModAction.GenericMod.Stabilizers.S [variable, in action]
ModAction.rT [variable, in action]
ModAction.to [variable, in action]
modact_is_action [lemma, in action]
modact_coset_astab [lemma, in action]
modact_is_groupAction [lemma, in action]
modact_faithful [lemma, in action]
modG [abbreviation, in mxrepresentation]
modgactE [lemma, in action]
modIp_mull [lemma, in poly]
modIp' [definition, in mxabelem]
modMp_eq [lemma, in poly]
modn [definition, in div]
modnn [lemma, in div]
modn_mul2m [lemma, in div]
modn_mod [lemma, in div]
modn_def [lemma, in div]
modn_partP [lemma, in prime]
modn_addl [lemma, in div]
modn_add2l [lemma, in div]
modn_mulr [lemma, in div]
modn_exp [lemma, in div]
modn_mull [lemma, in div]
modn_small [lemma, in div]
modn_coprime [lemma, in div]
modn_dvdm [lemma, in div]
modn_pmul2l [lemma, in div]
modn_addl_mul [lemma, in div]
modn_add2m [lemma, in div]
modn_mulml [lemma, in div]
modn_rec [definition, in div]
modn_addr [lemma, in div]
modn_addml [lemma, in div]
modn_addmr [lemma, in div]
modn_add2r [lemma, in div]
modn_mulmr [lemma, in div]
modn0 [lemma, in div]
modn1 [lemma, in div]
modn2 [lemma, in div]
modp [definition, in poly]
ModP [section, in sylow]
modpC [lemma, in poly]
modpp [lemma, in poly]
modp_size [lemma, in poly]
modp_spec [lemma, in poly]
ModP.aT [variable, in sylow]
ModP.D [variable, in sylow]
ModP.sT [variable, in sylow]
ModP.to [variable, in sylow]
modp0 [lemma, in poly]
modp1 [lemma, in poly]
ModularGroup [constructor, in extremal]
ModularGroupAction [section, in sylow]
ModularGroupAction.aT [variable, in sylow]
ModularGroupAction.D [variable, in sylow]
ModularGroupAction.p [variable, in sylow]
ModularGroupAction.R [variable, in sylow]
ModularGroupAction.rT [variable, in sylow]
ModularGroupAction.to [variable, in sylow]
ModularRepresentation [section, in mxabelem]
ModularRepresentation.charFp [variable, in mxabelem]
ModularRepresentation.F [variable, in mxabelem]
ModularRepresentation.G [variable, in mxabelem]
ModularRepresentation.gT [variable, in mxabelem]
ModularRepresentation.n [variable, in mxabelem]
ModularRepresentation.p [variable, in mxabelem]
ModularRepresentation.rG [variable, in mxabelem]
modular_gtype [definition, in extremal]
modular_group_classP [lemma, in extremal]
modular_group_structure [lemma, in extremal]
modular_group_generators [definition, in extremal]
modZp [lemma, in zmodp]
mod_groupAction [definition, in action]
mod_action [definition, in action]
mod0n [lemma, in div]
mod0p [lemma, in poly]
monic [definition, in poly]
monicX [lemma, in poly]
monicXn [lemma, in poly]
monic_neq0 [lemma, in poly]
monic_mull [lemma, in poly]
monic_mulr [lemma, in poly]
monic_exp [lemma, in poly]
monic_modp_add [lemma, in poly]
monic_factor [lemma, in poly]
monic_modp_mulmr [lemma, in poly]
monic_comreg [lemma, in poly]
monic_divp_mull [lemma, in poly]
monic1 [lemma, in poly]
Monoid [module, in bigop]
MonoidProperties [section, in bigop]
MonoidProperties.Abelian [section, in bigop]
MonoidProperties.Abelian.op [variable, in bigop]
MonoidProperties.idx [variable, in bigop]
MonoidProperties.Plain [section, in bigop]
MonoidProperties.Plain.op [variable, in bigop]
MonoidProperties.R [variable, in bigop]
Monoid.AddLaw [constructor, in bigop]
Monoid.add_law [record, in bigop]
Monoid.add_operator [projection, in bigop]
Monoid.clone_add_law [definition, in bigop]
Monoid.clone_mul_law [definition, in bigop]
Monoid.clone_com_law [definition, in bigop]
Monoid.clone_law [definition, in bigop]
Monoid.ComLaw [constructor, in bigop]
Monoid.CommutativeAxioms [section, in bigop]
Monoid.CommutativeAxioms.add [variable, in bigop]
Monoid.CommutativeAxioms.inv [variable, in bigop]
Monoid.CommutativeAxioms.mul [variable, in bigop]
Monoid.CommutativeAxioms.mulC [variable, in bigop]
Monoid.CommutativeAxioms.one [variable, in bigop]
Monoid.CommutativeAxioms.T [variable, in bigop]
Monoid.CommutativeAxioms.zero [variable, in bigop]
Monoid.com_operator [projection, in bigop]
Monoid.com_law [record, in bigop]
Monoid.Definitions [section, in bigop]
Monoid.Definitions.idm [variable, in bigop]
Monoid.Definitions.T [variable, in bigop]
Monoid.Law [constructor, in bigop]
Monoid.law [record, in bigop]
Monoid.mulC_zero [lemma, in bigop]
Monoid.mulC_id [lemma, in bigop]
Monoid.mulC_dist [lemma, in bigop]
Monoid.MulLaw [constructor, in bigop]
Monoid.mul_law [record, in bigop]
Monoid.mul_operator [projection, in bigop]
Monoid.operator [projection, in bigop]
Monoid.op_id [definition, in bigop]
Monoid.Theory.addmA [lemma, in bigop]
Monoid.Theory.addmAC [lemma, in bigop]
Monoid.Theory.addmC [lemma, in bigop]
Monoid.Theory.addmCA [lemma, in bigop]
Monoid.Theory.addm0 [lemma, in bigop]
Monoid.Theory.add0m [lemma, in bigop]
Monoid.Theory.iteropE [lemma, in bigop]
Monoid.Theory.mulmA [lemma, in bigop]
Monoid.Theory.mulmAC [lemma, in bigop]
Monoid.Theory.mulmC [lemma, in bigop]
Monoid.Theory.mulmCA [lemma, in bigop]
Monoid.Theory.mulm_addr [lemma, in bigop]
Monoid.Theory.mulm_addl [lemma, in bigop]
Monoid.Theory.mulm0 [lemma, in bigop]
Monoid.Theory.mulm1 [lemma, in bigop]
Monoid.Theory.mul0m [lemma, in bigop]
Monoid.Theory.mul1m [lemma, in bigop]
Monoid.Theory.simpm [definition, in bigop]
Monoid.Theory.Theory [section, in bigop]
Monoid.Theory.Theory.Add [section, in bigop]
Monoid.Theory.Theory.Add.add [variable, in bigop]
Monoid.Theory.Theory.Add.mul [variable, in bigop]
Monoid.Theory.Theory.Commutative [section, in bigop]
Monoid.Theory.Theory.Commutative.mul [variable, in bigop]
Monoid.Theory.Theory.idm [variable, in bigop]
Monoid.Theory.Theory.Mul [section, in bigop]
Monoid.Theory.Theory.Mul.mul [variable, in bigop]
Monoid.Theory.Theory.Plain [section, in bigop]
Monoid.Theory.Theory.Plain.mul [variable, in bigop]
Monoid.Theory.Theory.T [variable, in bigop]
monotone [definition, in ssrnat]
monotone_leqif [lemma, in ssrnat]
MonotonicFunctorTheory [section, in gfunctor]
MonotonicFunctorTheory.Composition [section, in gfunctor]
MonotonicFunctorTheory.Composition.F1 [variable, in gfunctor]
MonotonicFunctorTheory.Composition.F2 [variable, in gfunctor]
MonotonicFunctorTheory.F1 [variable, in gfunctor]
MonotonicFunctorTheory.F2 [variable, in gfunctor]
MoreGroupAction [section, in jordanholder]
MoreGroupAction.A [variable, in jordanholder]
MoreGroupAction.aT [variable, in jordanholder]
MoreGroupAction.D [variable, in jordanholder]
MoreGroupAction.rT [variable, in jordanholder]
MoreGroupAction.to [variable, in jordanholder]
MoreQuotientAction [section, in jordanholder]
MoreQuotientAction.A [variable, in jordanholder]
MoreQuotientAction.aT [variable, in jordanholder]
MoreQuotientAction.D [variable, in jordanholder]
MoreQuotientAction.rT [variable, in jordanholder]
MoreQuotientAction.to [variable, in jordanholder]
MoreSylow [section, in sylow]
MoreSylow.gT [variable, in sylow]
MoreSylow.p [variable, in sylow]
MorphAbelem [section, in abelian]
MorphAbelem.aT [variable, in abelian]
MorphAbelem.D [variable, in abelian]
MorphAbelem.f [variable, in abelian]
MorphAbelem.rT [variable, in abelian]
MorphAct [section, in action]
MorphAct.aT [variable, in action]
MorphAct.D [variable, in action]
MorphAct.phi [variable, in action]
MorphAct.rT [variable, in action]
morphAnd [abbreviation, in mxrepresentation]
morPhantom [abbreviation, in morphism]
MorPhantom [definition, in morphism]
morphic [definition, in morphism]
MorphicImage [section, in cyclic]
MorphicImage.aT [variable, in cyclic]
MorphicImage.D [variable, in cyclic]
MorphicImage.Dx [variable, in cyclic]
MorphicImage.f [variable, in cyclic]
MorphicImage.rT [variable, in cyclic]
MorphicImage.x [variable, in cyclic]
morphicP [lemma, in morphism]
morphic_aut [lemma, in automorphism]
Morphim [section, in pgroup]
morphim [definition, in morphism]
morphimD [lemma, in morphism]
morphimDG [lemma, in morphism]
morphimE [lemma, in morphism]
morphimEdom [lemma, in morphism]
morphimEsub [lemma, in morphism]
morphimF [lemma, in gfunctor]
morphimGI [lemma, in morphism]
morphimGK [lemma, in morphism]
morphimI [lemma, in morphism]
morphimIdom [lemma, in morphism]
morphimIG [lemma, in morphism]
morphimIim [lemma, in morphism]
MorphimInternalProd [section, in gproduct]
MorphimInternalProd.D [variable, in gproduct]
MorphimInternalProd.f [variable, in gproduct]
MorphimInternalProd.G [variable, in gproduct]
MorphimInternalProd.gT [variable, in gproduct]
MorphimInternalProd.H [variable, in gproduct]
MorphimInternalProd.K [variable, in gproduct]
MorphimInternalProd.rT [variable, in gproduct]
MorphimInternalProd.sGD [variable, in gproduct]
morphimJ [lemma, in morphism]
morphimK [lemma, in morphism]
morphimMl [lemma, in morphism]
morphimMr [lemma, in morphism]
morphimP [lemma, in morphism]
morphimR [lemma, in morphism]
morphimS [lemma, in morphism]
morphimSGK [lemma, in morphism]
morphimSK [lemma, in morphism]
MorphimSpec [constructor, in morphism]
morphimU [lemma, in morphism]
morphimV [lemma, in morphism]
morphimY [lemma, in morphism]
morphim_sdprodmr [lemma, in gproduct]
morphim_LdivT [lemma, in abelian]
morphim_cyclic [lemma, in cyclic]
morphim_spec [inductive, in morphism]
morphim_ker [lemma, in morphism]
morphim_cent1s [lemma, in morphism]
morphim_invm [lemma, in morphism]
morphim_quotm [lemma, in quotient]
morphim_groupset [lemma, in morphism]
morphim_cprodm [lemma, in gproduct]
morphim_sdprodml [lemma, in gproduct]
morphim_normG [lemma, in morphism]
morphim_sol [lemma, in nilpotent]
morphim_subnormG [lemma, in morphism]
morphim_Ohm [lemma, in abelian]
morphim_injm_eq1 [lemma, in morphism]
morphim_pnElem [lemma, in abelian]
morphim_p_group [lemma, in pgroup]
morphim_cent1 [lemma, in morphism]
morphim_abelian [lemma, in morphism]
morphim_sndX [lemma, in gproduct]
morphim_qisom_inj [lemma, in quotient]
morphim_fstX [lemma, in gproduct]
morphim_actm [lemma, in action]
morphim_fixP [lemma, in automorphism]
morphim_repr [definition, in mxrepresentation]
morphim_pgroup [lemma, in pgroup]
morphim_injG [lemma, in morphism]
morphim_pHall [lemma, in pgroup]
morphim_idm [lemma, in morphism]
morphim_group [definition, in morphism]
morphim_dprodm [lemma, in gproduct]
morphim_coprime_dprod [lemma, in gproduct]
morphim_cprod [lemma, in gproduct]
morphim_lcn [lemma, in nilpotent]
morphim_sdprodm [lemma, in gproduct]
morphim_p_index [lemma, in pgroup]
morphim_subcent [lemma, in morphism]
morphim_Zgroup [lemma, in sylow]
morphim_gen [lemma, in morphism]
morphim_mx [definition, in mxrepresentation]
morphim_ucn [lemma, in nilpotent]
morphim_coprime_sdprod [lemma, in gproduct]
morphim_Fitting [lemma, in maximal]
morphim_der [lemma, in commutator]
morphim_Ldiv [lemma, in abelian]
morphim_pcore_mod [lemma, in pgroup]
morphim_normal [lemma, in morphism]
morphim_norm [lemma, in morphism]
morphim_factm [lemma, in morphism]
morphim_pprodmr [lemma, in gproduct]
morphim_isom [lemma, in morphism]
morphim_dprodmr [lemma, in gproduct]
morphim_invmE [lemma, in morphism]
morphim_pprod [lemma, in gproduct]
morphim_pair1g [lemma, in gproduct]
morphim_mx_repr [lemma, in mxrepresentation]
morphim_Phi [lemma, in maximal]
morphim_abelem [lemma, in abelian]
morphim_odd [lemma, in pgroup]
morphim_grank [lemma, in abelian]
morphim_dprodml [lemma, in gproduct]
morphim_cents [lemma, in morphism]
morphim_pcore [lemma, in pgroup]
morphim_cprodml [lemma, in gproduct]
morphim_mx_abs_irr [lemma, in mxrepresentation]
morphim_pprodm [lemma, in gproduct]
morphim_subnorm [lemma, in morphism]
morphim_homg [lemma, in morphism]
morphim_trivm [lemma, in morphism]
morphim_pairg1 [lemma, in gproduct]
morphim_mxE [lemma, in mxrepresentation]
morphim_Sylow [lemma, in pgroup]
morphim_rank_abelian [lemma, in abelian]
morphim_subcent1 [lemma, in morphism]
morphim_qisom [lemma, in quotient]
morphim_nil [lemma, in nilpotent]
morphim_Hall [lemma, in pgroup]
morphim_Mho [lemma, in abelian]
morphim_setIpre [lemma, in morphism]
morphim_cprodmr [lemma, in gproduct]
morphim_pseries [lemma, in pgroup]
morphim_sub [lemma, in morphism]
morphim_restrm [lemma, in morphism]
morphim_set1 [lemma, in morphism]
morphim_norms [lemma, in morphism]
morphim_pSylow [lemma, in pgroup]
morphim_cent [lemma, in morphism]
morphim_center [lemma, in center]
morphim_cycle [lemma, in morphism]
morphim_inj [lemma, in morphism]
morphim_subnormal [lemma, in gseries]
morphim_conj [lemma, in automorphism]
morphim_p_rank_abelian [lemma, in abelian]
morphim_ifactm [lemma, in morphism]
morphim_mx_irr [lemma, in mxrepresentation]
morphim_pElem [lemma, in abelian]
morphim_pprodml [lemma, in gproduct]
morphim_comp [lemma, in morphism]
Morphim.aT [variable, in pgroup]
Morphim.D [variable, in pgroup]
Morphim.f [variable, in pgroup]
Morphim.rT [variable, in pgroup]
morphim0 [lemma, in morphism]
morphim1 [lemma, in morphism]
morphism [record, in morphism]
Morphism [constructor, in morphism]
Morphism [section, in bigop]
Morphism [section, in ssrfun]
morphism [library]
MorphismComposition [section, in morphism]
MorphismComposition.f [variable, in morphism]
MorphismComposition.g [variable, in morphism]
MorphismComposition.G [variable, in morphism]
MorphismComposition.gT [variable, in morphism]
MorphismComposition.H [variable, in morphism]
MorphismComposition.hT [variable, in morphism]
MorphismComposition.rT [variable, in morphism]
MorphismOps1 [section, in morphism]
MorphismOps1.aT [variable, in morphism]
MorphismOps1.D [variable, in morphism]
MorphismOps1.f [variable, in morphism]
MorphismOps1.rT [variable, in morphism]
MorphismStructure [section, in morphism]
MorphismStructure.A [variable, in morphism]
MorphismStructure.aT [variable, in morphism]
MorphismStructure.D [variable, in morphism]
MorphismStructure.f [variable, in morphism]
MorphismStructure.R [variable, in morphism]
MorphismStructure.rT [variable, in morphism]
MorphismStructure.x [variable, in morphism]
MorphismStructure.y [variable, in morphism]
MorphismTheory [section, in morphism]
MorphismTheory.aT [variable, in morphism]
MorphismTheory.D [variable, in morphism]
MorphismTheory.f [variable, in morphism]
MorphismTheory.Injective [section, in morphism]
MorphismTheory.Injective.injf [variable, in morphism]
MorphismTheory.rT [variable, in morphism]
morphism_2 [definition, in ssrfun]
morphism_for [definition, in morphism]
morphism_1 [definition, in ssrfun]
Morphism.aT [variable, in ssrfun]
Morphism.f [variable, in ssrfun]
Morphism.idx1 [variable, in bigop]
Morphism.idx2 [variable, in bigop]
Morphism.op1 [variable, in bigop]
Morphism.op2 [variable, in bigop]
Morphism.phi [variable, in bigop]
Morphism.phiM [variable, in bigop]
Morphism.phi_id [variable, in bigop]
Morphism.rT [variable, in ssrfun]
Morphism.R1 [variable, in bigop]
Morphism.R2 [variable, in bigop]
Morphism.sT [variable, in ssrfun]
morphJ [lemma, in morphism]
morphm [definition, in morphism]
morphM [lemma, in morphism]
morphmE [lemma, in morphism]
morphm_morphism [definition, in morphism]
MorphNil [section, in nilpotent]
MorphNil.aT [variable, in nilpotent]
MorphNil.D [variable, in nilpotent]
MorphNil.f [variable, in nilpotent]
MorphNil.rT [variable, in nilpotent]
MorphPcore [section, in pgroup]
MorphPcore.PcoreMod [section, in pgroup]
MorphPcore.PcoreMod.F [variable, in pgroup]
MorphPoly [section, in poly]
MorphPoly.aR [variable, in poly]
MorphPoly.pf [variable, in poly]
MorphPoly.rR [variable, in poly]
morphpre [definition, in morphism]
morphpreD [lemma, in morphism]
morphpreE [lemma, in morphism]
morphpreI [lemma, in morphism]
morphpreIdom [lemma, in morphism]
morphpreIim [lemma, in morphism]
morphpreJ [lemma, in morphism]
morphpreK [lemma, in morphism]
MorphPreMax [section, in gseries]
MorphPreMax.D [variable, in gseries]
MorphPreMax.f [variable, in gseries]
MorphPreMax.gT [variable, in gseries]
MorphPreMax.rT [variable, in gseries]
morphpreMl [lemma, in morphism]
morphpreMr [lemma, in morphism]
morphpreP [lemma, in morphism]
morphpreS [lemma, in morphism]
morphpreSK [lemma, in morphism]
morphpreT [lemma, in morphism]
morphpreU [lemma, in morphism]
morphpreV [lemma, in morphism]
morphpre_maximal_eq [lemma, in gseries]
morphpre_idm [lemma, in morphism]
morphpre_subcent1 [lemma, in morphism]
morphpre_factm [lemma, in morphism]
morphpre_set1 [lemma, in morphism]
morphpre_qisom [lemma, in quotient]
morphpre_mx_abs_irr [lemma, in mxrepresentation]
morphpre_subcent [lemma, in morphism]
morphpre_groupset [lemma, in morphism]
morphpre_proper [lemma, in morphism]
morphpre_repr [definition, in mxrepresentation]
morphpre_restrm [lemma, in morphism]
morphpre_group [definition, in morphism]
morphpre_comp [lemma, in morphism]
morphpre_invm [lemma, in morphism]
morphpre_ifactm [lemma, in morphism]
morphpre_cent1 [lemma, in morphism]
morphpre_maximal [lemma, in gseries]
morphpre_cent1s [lemma, in morphism]
morphpre_normal [lemma, in morphism]
morphpre_cent [lemma, in morphism]
morphpre_gen [lemma, in morphism]
morphpre_norm [lemma, in morphism]
morphpre_subnorm [lemma, in morphism]
morphpre_cents [lemma, in morphism]
morphpre_norms [lemma, in morphism]
morphpre_mx_irr [lemma, in mxrepresentation]
morphpre_inj [lemma, in morphism]
morphpre_quotm [lemma, in quotient]
morphpre_mx_repr [lemma, in mxrepresentation]
morphpre0 [lemma, in morphism]
morphR [lemma, in morphism]
MorphSol [section, in nilpotent]
MorphSol.D [variable, in nilpotent]
MorphSol.f [variable, in nilpotent]
MorphSol.G [variable, in nilpotent]
MorphSol.gT [variable, in nilpotent]
MorphSol.rT [variable, in nilpotent]
MorphSubNormal [section, in gseries]
MorphSubNormal.gT [variable, in gseries]
morphV [lemma, in morphism]
morphX [lemma, in morphism]
morph_generator [lemma, in cyclic]
morph_constt [lemma, in pgroup]
morph_dom_groupset [lemma, in morphism]
morph_dom_group [definition, in morphism]
morph_injm_eq1 [lemma, in morphism]
morph_order [lemma, in cyclic]
morph_act [definition, in action]
morph_action [definition, in action]
morph_p_elt [lemma, in pgroup]
morph1 [lemma, in morphism]
mulg [definition, in fingroup]
mulgA [lemma, in fingroup]
mulgI [lemma, in fingroup]
mulGid [lemma, in fingroup]
mulGidPl [lemma, in fingroup]
mulGidPr [lemma, in fingroup]
mulgK [lemma, in fingroup]
mulgKV [lemma, in fingroup]
mulgm [definition, in gproduct]
mulgmP [lemma, in gproduct]
mulgr_action [definition, in action]
mulgS [lemma, in fingroup]
mulGS [lemma, in fingroup]
mulGSgid [lemma, in fingroup]
mulGSid [lemma, in fingroup]
mulgSS [lemma, in fingroup]
mulGsubP [lemma, in fingroup]
mulgT [abbreviation, in fingroup]
mulgT [abbreviation, in fingroup]
mulgU [lemma, in fingroup]
mulgV [lemma, in fingroup]
mulG_subr [lemma, in fingroup]
mulG_subl [lemma, in fingroup]
mulg_nil [lemma, in nilpotent]
mulg_exp_card_rcosets [lemma, in finmodule]
mulg_set1 [lemma, in fingroup]
mulG_subG [lemma, in fingroup]
mulg_normal_maximal [lemma, in gseries]
mulG_sub [lemma, in fingroup]
mulg_subl [lemma, in fingroup]
mulg_subr [lemma, in fingroup]
mulg0 [lemma, in gproduct]
mulg1 [lemma, in fingroup]
mulIg [lemma, in fingroup]
mulKg [lemma, in fingroup]
mulKmx [lemma, in matrix]
mulKn [lemma, in div]
mulKVg [lemma, in fingroup]
mulKVmx [lemma, in matrix]
mulmx [definition, in matrix]
mulmxA [lemma, in matrix]
mulmxE [lemma, in matrix]
mulmxK [lemma, in matrix]
mulmxKpV [lemma, in mxalgebra]
mulmxKV [lemma, in matrix]
mulmxKV_ker [lemma, in mxalgebra]
mulmxN [lemma, in matrix]
mulmxnE [lemma, in matrix]
mulmxr [abbreviation, in matrix]
mulmxr [abbreviation, in matrix]
mulmxr_is_linear [lemma, in matrix]
mulmxr_head [definition, in matrix]
mulmxr_linear [definition, in matrix]
mulmxr_additive [definition, in matrix]
mulmxV [lemma, in matrix]
mulmx_subl [lemma, in matrix]
mulmx_base [lemma, in mxalgebra]
mulmx_diag [lemma, in matrix]
mulmx_sumr [lemma, in matrix]
mulmx_addl [lemma, in matrix]
mulmx_ebase [lemma, in mxalgebra]
mulmx_block [lemma, in matrix]
mulmx_ker [lemma, in mxalgebra]
mulmx_sum_row [lemma, in matrix]
mulmx_is_scalable [lemma, in matrix]
mulmx_linear [definition, in matrix]
mulmx_additive [definition, in matrix]
mulmx_sub [lemma, in mxalgebra]
mulmx_max_rank [lemma, in mxalgebra]
mulmx_addr [lemma, in matrix]
mulmx_suml [lemma, in matrix]
mulmx_subr [lemma, in matrix]
mulmx_coker [lemma, in mxalgebra]
mulmx0 [lemma, in matrix]
mulmx0_rank_max [lemma, in mxalgebra]
mulmx1 [lemma, in matrix]
mulmx1C [lemma, in matrix]
mulmx1_min [lemma, in matrix]
mulmx1_min_rank [lemma, in mxalgebra]
mulmx1_unit [lemma, in matrix]
muln [definition, in ssrnat]
mulnA [lemma, in ssrnat]
mulnAC [lemma, in ssrnat]
mulnb [lemma, in ssrnat]
mulnC [lemma, in ssrnat]
mulnCA [lemma, in ssrnat]
mulnE [lemma, in ssrnat]
mulnK [lemma, in div]
mulNmx [lemma, in matrix]
mulnn [lemma, in ssrnat]
mulnS [lemma, in ssrnat]
mulnSr [lemma, in ssrnat]
muln_lcm_gcd [lemma, in div]
muln_rec [definition, in ssrnat]
muln_gcdr [lemma, in div]
muln_gcdl [lemma, in div]
muln_eq0 [lemma, in ssrnat]
muln_lcmr [lemma, in div]
muln_subr [lemma, in ssrnat]
muln_muloid [definition, in bigop]
muln_comoid [definition, in bigop]
muln_monoid [definition, in bigop]
muln_subl [lemma, in ssrnat]
muln_gt0 [lemma, in ssrnat]
muln_addl [lemma, in ssrnat]
muln_lcml [lemma, in div]
muln_addr [lemma, in ssrnat]
muln0 [lemma, in ssrnat]
muln1 [lemma, in ssrnat]
muln2 [lemma, in ssrnat]
mulSg [lemma, in fingroup]
mulSG [lemma, in fingroup]
mulSgGid [lemma, in fingroup]
mulSGid [lemma, in fingroup]
mulsgP [lemma, in fingroup]
mulsmx [definition, in mxalgebra]
mulsmxA [lemma, in mxalgebra]
mulsmxP [lemma, in mxalgebra]
mulsmxS [lemma, in mxalgebra]
mulsmx_addl [lemma, in mxalgebra]
mulsmx_addr [lemma, in mxalgebra]
mulsmx_subP [lemma, in mxalgebra]
mulsmx0 [lemma, in mxalgebra]
mulSn [lemma, in ssrnat]
mulSnr [lemma, in ssrnat]
muls_eqmx [lemma, in mxalgebra]
muls0mx [lemma, in mxalgebra]
multE [lemma, in ssrnat]
multn [definition, in div]
mulUg [lemma, in fingroup]
mulVg [lemma, in fingroup]
mulVmx [lemma, in matrix]
mul_poly [definition, in poly]
mul_subG [lemma, in fingroup]
mul_col_row [lemma, in matrix]
mul_delta_mx_0 [lemma, in matrix]
mul_pid_mx_copid [lemma, in matrix]
mul_delta_mx [lemma, in matrix]
mul_block_col [lemma, in matrix]
mul_poly_addr [lemma, in poly]
mul_delta_mx_cond [lemma, in matrix]
mul_pid_mx [lemma, in matrix]
mul_polyA [lemma, in poly]
mul_Sm_binm [lemma, in binomial]
mul_mx_diag [lemma, in matrix]
mul_cardG [lemma, in fingroup]
mul_poly_addl [lemma, in poly]
mul_diag_mx [lemma, in matrix]
mul_mx_scalar [lemma, in matrix]
mul_rV_lin1 [lemma, in matrix]
mul_mx_row [lemma, in matrix]
mul_col_perm [lemma, in matrix]
mul_copid_mx_pid [lemma, in matrix]
mul_polyC [lemma, in poly]
mul_vec_lin [lemma, in matrix]
mul_mx_adj [lemma, in matrix]
mul_vec_lin_row [lemma, in matrix]
mul_col_mx [lemma, in matrix]
mul_poly1 [lemma, in poly]
mul_rV_lin [lemma, in matrix]
mul_adj_mx [lemma, in matrix]
mul_card_Ohm_Mho_abelian [lemma, in abelian]
mul_row_col [lemma, in matrix]
mul_row_perm [lemma, in matrix]
mul_scalar_mx [lemma, in matrix]
mul_row_block [lemma, in matrix]
mul_1poly [lemma, in poly]
mul_xcol [lemma, in matrix]
mul0g [lemma, in gproduct]
mul0mx [lemma, in matrix]
mul0n [lemma, in ssrnat]
mul1g [lemma, in fingroup]
mul1mx [lemma, in matrix]
mul1n [lemma, in ssrnat]
mul2n [lemma, in ssrnat]
MV [abbreviation, in matrix]
mxabelem [library]
mxalgebra [library]
mxdirect [abbreviation, in mxalgebra]
mxdirect [abbreviation, in mxalgebra]
mxdirectE [lemma, in mxalgebra]
mxdirectEgeq [lemma, in mxalgebra]
mxdirectP [lemma, in mxalgebra]
mxdirect_sum_eigenspace [lemma, in mxalgebra]
mxdirect_trivial [lemma, in mxalgebra]
mxdirect_addsP [lemma, in mxalgebra]
mxdirect_sumsE [lemma, in mxalgebra]
mxdirect_sums_recP [definition, in mxalgebra]
mxdirect_def [definition, in mxalgebra]
mxdirect_adds_center [lemma, in mxalgebra]
mxdirect_addsE [lemma, in mxalgebra]
mxdirect_sumsP [lemma, in mxalgebra]
mxdirect_sums_center [lemma, in mxalgebra]
mxE [lemma, in matrix]
mxeq2vseq [lemma, in vector]
MxIso [constructor, in mxrepresentation]
mxminpoly [definition, in mxpoly]
mxminpoly_map [lemma, in mxpoly]
mxminpoly_linear_is_scalar [lemma, in mxpoly]
mxminpoly_min [lemma, in mxpoly]
mxminpoly_nonconstant [lemma, in mxpoly]
mxminpoly_monic [lemma, in mxpoly]
mxminpoly_dvd_char [lemma, in mxpoly]
mxmodule [definition, in mxrepresentation]
mxmoduleP [lemma, in mxrepresentation]
mxmodule_eqg [lemma, in mxrepresentation]
mxmodule_subg [lemma, in mxrepresentation]
mxmodule_morphpre [lemma, in mxrepresentation]
mxmodule_form [definition, in mxrepresentation]
mxmodule_envelop [lemma, in mxrepresentation]
mxmodule_eigenvector [lemma, in mxrepresentation]
mxmodule_quo [lemma, in mxrepresentation]
mxmodule_conj [lemma, in mxrepresentation]
mxmodule_morphim [lemma, in mxrepresentation]
mxmodule_form_qf [lemma, in mxrepresentation]
mxmodule_map [lemma, in mxrepresentation]
mxmodule_trans [lemma, in mxrepresentation]
mxmodule0 [lemma, in mxrepresentation]
mxmodule1 [lemma, in mxrepresentation]
mxnonsimple [definition, in mxrepresentation]
mxnonsimpleP [lemma, in mxrepresentation]
mxnonsimple_sat [definition, in mxrepresentation]
mxnonsimple_form [definition, in mxrepresentation]
mxopE [definition, in mxalgebra]
mxpoly [library]
mxrank [definition, in mxalgebra]
mxrankE [lemma, in mxalgebra]
mxrankMfree [lemma, in mxalgebra]
mxrankM_maxr [lemma, in mxalgebra]
mxrankM_maxl [lemma, in mxalgebra]
mxrankS [lemma, in mxalgebra]
mxrank_leqif_eq [lemma, in mxalgebra]
mxrank_delta [lemma, in mxalgebra]
mxrank_in_factmod [lemma, in mxrepresentation]
mxrank_adds_leqif [lemma, in mxalgebra]
mxrank_Frobenius [lemma, in mxalgebra]
mxrank_cap_compl [lemma, in mxalgebra]
mxrank_scale_nz [lemma, in mxalgebra]
mxrank_rsim [lemma, in mxrepresentation]
mxrank_gen [lemma, in mxalgebra]
mxrank_add [lemma, in mxalgebra]
mxrank_in_submod [lemma, in mxrepresentation]
mxrank_mul_min [lemma, in mxalgebra]
mxrank_ker [lemma, in mxalgebra]
mxrank_scale [lemma, in mxalgebra]
mxrank_compl [lemma, in mxalgebra]
mxrank_iso [lemma, in mxrepresentation]
mxrank_disjoint_sum [lemma, in mxalgebra]
mxrank_coker [lemma, in mxalgebra]
mxrank_opp [lemma, in mxalgebra]
mxrank_leqif_sup [lemma, in mxalgebra]
mxrank_sum_cap [lemma, in mxalgebra]
mxrank_sum_leqif [lemma, in mxalgebra]
mxrank_eq0 [lemma, in mxalgebra]
mxrank_mul_ker [lemma, in mxalgebra]
mxrank_tr [lemma, in mxalgebra]
mxrank_unit [lemma, in mxalgebra]
mxrank_injP [lemma, in mxalgebra]
mxrank_map [lemma, in mxalgebra]
mxrank0 [lemma, in mxalgebra]
mxrank1 [lemma, in mxalgebra]
MxRepresentation [constructor, in mxrepresentation]
mxrepresentation [library]
MxReprSim [constructor, in mxrepresentation]
mxring [definition, in mxalgebra]
mxring_id [definition, in mxalgebra]
mxring_id_uniq [lemma, in mxalgebra]
mxring_idP [lemma, in mxalgebra]
mxsemisimple [inductive, in mxrepresentation]
MxSemisimple [constructor, in mxrepresentation]
mxsemisimpleS [lemma, in mxrepresentation]
mxsemisimple_reducible [lemma, in mxrepresentation]
mxsemisimple_module [lemma, in mxrepresentation]
mxsemisimple0 [lemma, in mxrepresentation]
mxsimple [definition, in mxrepresentation]
mxsimpleP [lemma, in mxrepresentation]
mxsimple_isoP [lemma, in mxrepresentation]
mxsimple_abelian_linear [lemma, in mxrepresentation]
mxsimple_iso_simple [lemma, in mxrepresentation]
mxsimple_exists [lemma, in mxrepresentation]
mxsimple_iso [definition, in mxrepresentation]
mxsimple_semisimple [lemma, in mxrepresentation]
mxsimple_morphim [lemma, in mxrepresentation]
mxsimple_cyclic [lemma, in mxrepresentation]
mxsimple_module [lemma, in mxrepresentation]
mxsimple_subg [lemma, in mxrepresentation]
mxsimple_map [lemma, in mxrepresentation]
mxsimple_eqg [lemma, in mxrepresentation]
mxsplits [inductive, in mxrepresentation]
MxSplits [constructor, in mxrepresentation]
Mxsum [constructor, in mxalgebra]
mxsum_val [projection, in mxalgebra]
mxsum_rank [projection, in mxalgebra]
mxsum_expr [record, in mxalgebra]
mxsum_spec [inductive, in mxalgebra]
mxtrace [definition, in matrix]
mxtraceD [lemma, in matrix]
mxtraceZ [lemma, in matrix]
mxtrace_Socle [lemma, in mxrepresentation]
mxtrace_submod1 [lemma, in mxrepresentation]
mxtrace_regular [lemma, in mxrepresentation]
mxtrace_rsim [lemma, in mxrepresentation]
mxtrace_mulC [lemma, in matrix]
mxtrace_block [lemma, in matrix]
mxtrace_tr [lemma, in matrix]
mxtrace_diag [lemma, in matrix]
mxtrace_linear [definition, in matrix]
mxtrace_additive [definition, in matrix]
mxtrace_scalar [lemma, in matrix]
mxtrace_component [lemma, in mxrepresentation]
mxtrace_dadd_mod [lemma, in mxrepresentation]
mxtrace_dsum_mod [lemma, in mxrepresentation]
mxtrace_sub_fact_mod [lemma, in mxrepresentation]
mxtrace_is_linear [lemma, in matrix]
mxtrace0 [lemma, in matrix]
mxtrace1 [lemma, in matrix]
mxvec [definition, in matrix]
mxvecE [lemma, in matrix]
mxvecK [lemma, in matrix]
mxvec_eq0 [lemma, in matrix]
mxvec_delta [lemma, in matrix]
mxvec_index [definition, in matrix]
mxvec_is_linear [definition, in matrix]
mxvec_indexP [lemma, in matrix]
mxvec_bij [lemma, in vector]
mxvec_cast [lemma, in matrix]
mxvec_linear [definition, in matrix]
mxvec_additive [definition, in matrix]
Mxy [definition, in extremal]
mx_abs_irr_cent_scalar [lemma, in mxrepresentation]
mx_iso [inductive, in mxrepresentation]
mx_factmod_sub [lemma, in mxrepresentation]
mx_iso_module [lemma, in mxrepresentation]
mx_JordanHolder [lemma, in mxrepresentation]
mx_abs_irrW [lemma, in mxrepresentation]
mx_faithful [definition, in mxrepresentation]
mx_poly_ring_isom [lemma, in mxpoly]
mx_rsim_irr [lemma, in mxrepresentation]
mx_Schur_inj [lemma, in mxrepresentation]
mx_series_repr_irr [lemma, in mxrepresentation]
mx_inv_hornerK [lemma, in mxpoly]
mx_Fp_stable [lemma, in mxabelem]
mx_irrP [lemma, in mxrepresentation]
mx_rsim_trans [lemma, in mxrepresentation]
mx_Jacobson_density [lemma, in mxrepresentation]
mx_repr [definition, in mxrepresentation]
mx_rsim_factmod [lemma, in mxrepresentation]
mx_subseries_module [lemma, in mxrepresentation]
mx_rsim_refl [lemma, in mxrepresentation]
mx_faithful_irr_abelian_cyclic [lemma, in mxrepresentation]
mx_iso_sym [lemma, in mxrepresentation]
mx_absolutely_irreducible [definition, in mxrepresentation]
mx_iso_component [lemma, in mxrepresentation]
mx_inv_horner [definition, in mxpoly]
mx_completely_reducible [definition, in mxrepresentation]
mx_series [abbreviation, in mxrepresentation]
mx_rsim_abs_irr [lemma, in mxrepresentation]
mx_reducibleS [lemma, in mxrepresentation]
mx_Schur_iso [lemma, in mxrepresentation]
mx_Schur [lemma, in mxrepresentation]
mx_rsim_faithful [lemma, in mxrepresentation]
mx_subseries [definition, in mxrepresentation]
mx_repr_groupAction [definition, in mxabelem]
mx_repr_action [definition, in mxabelem]
mx_iso_refl [lemma, in mxrepresentation]
mx_rsim_iso [lemma, in mxrepresentation]
mx_repr_action_faithful [lemma, in mxabelem]
mx_repr_actE [lemma, in mxabelem]
mx_iso_trans [lemma, in mxrepresentation]
mx_rsim [inductive, in mxrepresentation]
mx_subseries_module' [lemma, in mxrepresentation]
mx_composition_series [definition, in mxrepresentation]
mx_reducible_semisimple [lemma, in mxrepresentation]
mx_faithful_irr_center_cyclic [lemma, in mxrepresentation]
mx_series_lt [lemma, in mxrepresentation]
mx_repr_is_groupAction [lemma, in mxabelem]
mx_repr_is_action [lemma, in mxabelem]
mx_faithful_inj [lemma, in mxrepresentation]
mx_JordanHolder_max [lemma, in mxrepresentation]
mx_Schur_onto [lemma, in mxrepresentation]
mx_vec_lin [lemma, in matrix]
mx_Schreier [lemma, in mxrepresentation]
mx_ideal [definition, in mxalgebra]
mx_irreducible [definition, in mxrepresentation]
mx_rsim_map [lemma, in mxrepresentation]
mx_Schur_inj_iso [lemma, in mxrepresentation]
mx_root_minpoly [lemma, in mxpoly]
mx_rsim_sym [lemma, in mxrepresentation]
mx_irr_map [lemma, in mxrepresentation]
mx_abs_irrP [lemma, in mxrepresentation]
mx_inv_horner0 [lemma, in mxpoly]
mx_of_lapp [definition, in vector]
mx_second_rsim [lemma, in mxrepresentation]
mx_val [definition, in matrix]
mx_representation [record, in mxrepresentation]
mx_irr_abelian_linear [lemma, in mxrepresentation]
mx_Maschke [lemma, in mxrepresentation]
mx_iso_simple [lemma, in mxrepresentation]
mx_Fp_abelem [lemma, in mxabelem]
mx_rsim_in_submod [lemma, in mxrepresentation]
mx_JordanHolder_exists [lemma, in mxrepresentation]
mx_butterfly [lemma, in mxrepresentation]
mx_rV_lin [lemma, in matrix]
mx_repr_act [definition, in mxabelem]
mx_rsim_def [lemma, in mxrepresentation]
mx_series_rcons [lemma, in mxrepresentation]
mx'_cast [lemma, in matrix]
mx0_is_scalar [lemma, in matrix]
mx1_sum_delta [lemma, in matrix]
mx11_scalar [lemma, in matrix]
mx2vs [definition, in vector]
mx2vsD [lemma, in vector]
mx2vsDl [lemma, in vector]
mx2vsDr [lemma, in vector]
mx2vsf [lemma, in vector]
mx2vsK [lemma, in vector]
mx2vs0 [lemma, in vector]
My [definition, in extremal]



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (14626 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (165 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (112 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7292 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (250 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (390 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (84 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3144 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (126 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2221 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (53 entries)