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

(75560 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

(1797 entries)

Binder 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

(45699 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

(379 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

(3950 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

(91 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

(14168 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

(225 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

(135 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

(453 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

(1368 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

(869 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

(6133 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

(248 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]
MapIota [constructor, in mathcomp.ssreflect.seq]
mapK [lemma, in mathcomp.ssreflect.seq]
MapKermxPoly [section, in mathcomp.algebra.mxpoly]
MapKermxPoly.aF [variable, in mathcomp.algebra.mxpoly]
MapKermxPoly.f [variable, in mathcomp.algebra.mxpoly]
MapKermxPoly.rF [variable, in mathcomp.algebra.mxpoly]
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_orthonormal [lemma, in mathcomp.character.vcharacter]
map_pairwise_orthogonal [lemma, in mathcomp.character.vcharacter]
map_poly_divzK [lemma, in mathcomp.algebra.intdiv]
map_bseq [definition, in mathcomp.ssreflect.tuple]
map_bseqP [lemma, in mathcomp.ssreflect.tuple]
map_tuple [definition, in mathcomp.ssreflect.tuple]
map_tupleP [lemma, in mathcomp.ssreflect.tuple]
map_tnth_enum [lemma, in mathcomp.ssreflect.tuple]
map_allpairs [lemma, in mathcomp.ssreflect.seq]
map_reshape [lemma, in mathcomp.ssreflect.seq]
map_flatten [lemma, in mathcomp.ssreflect.seq]
map_nth_iota [lemma, in mathcomp.ssreflect.seq]
map_nth_iota0 [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_minPoly [lemma, in mathcomp.field.fieldext]
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_rmorphism [definition, 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_additive [definition, in mathcomp.algebra.matrix]
map_mx_sum [definition, in mathcomp.algebra.matrix]
map_mxB [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_mx_id [lemma, in mathcomp.algebra.matrix]
map_mx_id_in [lemma, in mathcomp.algebra.matrix]
map_mx_comp [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_mxsub [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_geigenspace [lemma, in mathcomp.algebra.mxpoly]
map_kermxpoly [lemma, in mathcomp.algebra.mxpoly]
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_cfAut_free [lemma, in mathcomp.character.classfun]
map_orthogonal [lemma, in mathcomp.character.classfun]
map_path [lemma, in mathcomp.ssreflect.path]
map_sort [lemma, in mathcomp.ssreflect.path]
map_merge [lemma, in mathcomp.ssreflect.path]
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_repr [definition, 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_div_annihilantP [lemma, in mathcomp.algebra.polyXY]
map_sub_annihilantP [lemma, in mathcomp.algebra.polyXY]
map_Qnum_poly [lemma, in mathcomp.field.algnum]
map_preim [lemma, in mathcomp.ssreflect.fintype]
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_poly_lrmorphism [definition, in mathcomp.algebra.poly]
map_poly_linear [definition, in mathcomp.algebra.poly]
map_polyZ [lemma, in mathcomp.algebra.poly]
map_poly_rmorphism [definition, in mathcomp.algebra.poly]
map_poly_is_rmorphism [lemma, in mathcomp.algebra.poly]
map_polyC [lemma, in mathcomp.algebra.poly]
map_poly_additive [definition, 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_filter [lemma, 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_rcons [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_sort_in [lemma, in mathcomp.ssreflect.path]
mask_sort [lemma, in mathcomp.ssreflect.path]
mask_enum_ord [lemma, in mathcomp.ssreflect.fintype]
Mask.n0 [variable, in mathcomp.ssreflect.seq]
Mask.T [variable, in mathcomp.ssreflect.seq]
mask0 [lemma, in mathcomp.ssreflect.seq]
mask0s [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.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_finFieldType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_finIdomainType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_finComUnitRingType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_finUnitRingType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_finComRingType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_finRingType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_finGroupType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_baseFinGroupType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_finZmodType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_subFinType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_finType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_finMixin [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_subCountType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_countType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_countMixin [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_decFieldType [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_repr [definition, 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_rmorphism [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_additive [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_is_rmorphism [lemma, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_fieldType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_idomainType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_idomainMixin [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_fieldMixin [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_comUnitRingType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_unitRingType [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_comRingType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_ringType [definition, 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_zmodType [definition, 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_choiceType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_choiceMixin [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_eqType [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_eqMixin [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.gen_subType [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_rmorphism [definition, in mathcomp.character.mxrepresentation]
MatrixGenField.mxval_is_multiplicative [lemma, in mathcomp.character.mxrepresentation]
MatrixGenField.mxval_additive [definition, 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.Induction [section, 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_finUnitRingType [definition, in mathcomp.algebra.matrix]
matrix_countUnitRingType [definition, in mathcomp.algebra.matrix]
matrix_unitAlg [definition, in mathcomp.algebra.matrix]
matrix_unitRing [definition, in mathcomp.algebra.matrix]
matrix_unitRingMixin [definition, in mathcomp.algebra.matrix]
matrix_finAlgType [definition, in mathcomp.algebra.matrix]
matrix_algType [definition, in mathcomp.algebra.matrix]
matrix_finLalgType [definition, in mathcomp.algebra.matrix]
matrix_finRingType [definition, in mathcomp.algebra.matrix]
matrix_finLmodType [definition, in mathcomp.algebra.matrix]
matrix_countRingType [definition, in mathcomp.algebra.matrix]
matrix_countZmodType [definition, in mathcomp.algebra.matrix]
matrix_lAlgType [definition, in mathcomp.algebra.matrix]
matrix_ringType [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_lmodType [definition, in mathcomp.algebra.matrix]
matrix_lmodMixin [definition, in mathcomp.algebra.matrix]
matrix_finGroupType [definition, in mathcomp.algebra.matrix]
matrix_baseFinGroupType [definition, in mathcomp.algebra.matrix]
matrix_finZmodType [definition, in mathcomp.algebra.matrix]
matrix_eq0 [lemma, in mathcomp.algebra.matrix]
matrix_zmodType [definition, in mathcomp.algebra.matrix]
matrix_zmodMixin [definition, in mathcomp.algebra.matrix]
matrix_ind [definition, in mathcomp.algebra.matrix]
matrix_rec [definition, in mathcomp.algebra.matrix]
matrix_rect [definition, in mathcomp.algebra.matrix]
matrix_subFinType [definition, in mathcomp.algebra.matrix]
matrix_finType [definition, in mathcomp.algebra.matrix]
matrix_finMixin [definition, in mathcomp.algebra.matrix]
matrix_subCountType [definition, in mathcomp.algebra.matrix]
matrix_countType [definition, in mathcomp.algebra.matrix]
matrix_countMixin [definition, in mathcomp.algebra.matrix]
matrix_choiceType [definition, in mathcomp.algebra.matrix]
matrix_choiceMixin [definition, in mathcomp.algebra.matrix]
matrix_eqType [definition, in mathcomp.algebra.matrix]
matrix_eqMixin [definition, in mathcomp.algebra.matrix]
matrix_unlockable [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_subType [definition, in mathcomp.algebra.matrix]
matrix_vectType [definition, in mathcomp.algebra.vector]
matrix_vectMixin [definition, in mathcomp.algebra.vector]
matrix_vect_iso [lemma, in mathcomp.algebra.vector]
matrix_FalgType [definition, in mathcomp.field.falgebra]
matrix_modr [lemma, in mathcomp.algebra.mxalgebra]
matrix_modl [lemma, in mathcomp.algebra.mxalgebra]
matrix0Pn [lemma, in mathcomp.algebra.matrix]
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]
maxnMl [lemma, in mathcomp.ssreflect.ssrnat]
maxnMr [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_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]
maxn_addoid [definition, in mathcomp.ssreflect.bigop]
maxn_comoid [definition, in mathcomp.ssreflect.bigop]
maxn_monoid [definition, in mathcomp.ssreflect.bigop]
maxn0 [lemma, in mathcomp.ssreflect.ssrnat]
MaxProps [section, in mathcomp.solvable.gseries]
MaxProps.gT [variable, in mathcomp.solvable.gseries]
maxrankfun [definition, in mathcomp.algebra.mxalgebra]
maxrankfun_inj [lemma, in mathcomp.algebra.mxalgebra]
MaxRoots [section, in mathcomp.algebra.poly]
MaxRoots.R [variable, in mathcomp.algebra.poly]
maxrowsub_full [lemma, in mathcomp.algebra.mxalgebra]
maxrowsub_free [lemma, in mathcomp.algebra.mxalgebra]
maxr_rat [lemma, in mathcomp.algebra.rat]
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_cofix [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_pgroup_Sylow [lemma, in mathcomp.solvable.sylow]
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_card_abelian [lemma, in mathcomp.solvable.abelian]
max_cfRepr_mx1 [lemma, in mathcomp.character.character]
max_cfRepr_norm_scalar [lemma, in mathcomp.character.character]
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]
max0n [lemma, in mathcomp.ssreflect.ssrnat]
mA:145 [binder, in mathcomp.character.mxabelem]
mA:248 [binder, in mathcomp.ssreflect.fintype]
mA:42 [binder, in mathcomp.ssreflect.fintype]
mA:556 [binder, in mathcomp.ssreflect.fintype]
mA:68 [binder, in mathcomp.ssreflect.fintype]
mA:97 [binder, in mathcomp.ssreflect.finset]
mbcs:2309 [binder, in mathcomp.algebra.ssralg]
mCFD:169 [binder, in mathcomp.character.classfun]
mCFR:171 [binder, in mathcomp.character.classfun]
mc:131 [binder, in mathcomp.algebra.ssrnum]
mD:137 [binder, in mathcomp.ssreflect.finfun]
mD:147 [binder, in mathcomp.ssreflect.finfun]
mD:47 [binder, in mathcomp.algebra.ring_quotient]
mD:529 [binder, in mathcomp.ssreflect.finset]
meet_Ohm1 [lemma, in mathcomp.solvable.abelian]
meet_center_nil [lemma, in mathcomp.solvable.nilpotent]
MemAllPairs [section, in mathcomp.ssreflect.seq]
MemAllPairs.R [variable, in mathcomp.ssreflect.seq]
MemAllPairs.S [variable, in mathcomp.ssreflect.seq]
MemAllPairs.T [variable, in mathcomp.ssreflect.seq]
membsE [lemma, in mathcomp.ssreflect.tuple]
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]
memNindex [lemma, in mathcomp.ssreflect.seq]
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_rcosetV [lemma, in mathcomp.fingroup.fingroup]
memV_lcosetV [lemma, in mathcomp.fingroup.fingroup]
memV_invg [lemma, in mathcomp.fingroup.fingroup]
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_submodPred [definition, in mathcomp.algebra.vector]
memv_zmodPred [definition, in mathcomp.algebra.vector]
memv_addrPred [definition, in mathcomp.algebra.vector]
memv_opprPred [definition, in mathcomp.algebra.vector]
memv_submod_closed [lemma, in mathcomp.algebra.vector]
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_quotient [lemma, in mathcomp.fingroup.quotient]
mem_repr_coset [lemma, in mathcomp.fingroup.quotient]
mem_zchar [lemma, in mathcomp.character.vcharacter]
mem_zchar_on [lemma, in mathcomp.character.vcharacter]
mem_porbit [lemma, in mathcomp.fingroup.perm]
mem_miditv [lemma, in mathcomp.algebra.interval]
mem_tnth [lemma, in mathcomp.ssreflect.tuple]
mem_permutations [lemma, in mathcomp.ssreflect.seq]
mem_allpairs [lemma, in mathcomp.ssreflect.seq]
mem_allpairs_rconsr [lemma, in mathcomp.ssreflect.seq]
mem_allpairs_consr [lemma, in mathcomp.ssreflect.seq]
mem_allpairs_catr [lemma, in mathcomp.ssreflect.seq]
mem_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
mem_infix [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_predType [definition, in mathcomp.ssreflect.seq]
mem_seq [definition, in mathcomp.ssreflect.seq]
mem_Zp [lemma, in mathcomp.algebra.zmodp]
mem_imset2_eq [abbreviation, in mathcomp.ssreflect.finset]
mem_imset_eq [abbreviation, in mathcomp.ssreflect.finset]
mem_pblock [lemma, in mathcomp.ssreflect.finset]
mem_imset2 [lemma, in mathcomp.ssreflect.finset]
mem_imset [lemma, in mathcomp.ssreflect.finset]
mem_galNorm [lemma, in mathcomp.field.galois]
mem_galTrace [lemma, in mathcomp.field.galois]
mem_fixedFieldP [lemma, in