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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(565 entries)

---

L

Lagrange [lemma, in mathcomp.fingroup.fingroup]
Lagrange [section, in mathcomp.fingroup.fingroup]
lagrange [definition, in mathcomp.algebra.qpoly]
lagrangeE [lemma, in mathcomp.algebra.qpoly]
LagrangeI [lemma, in mathcomp.fingroup.fingroup]
LagrangeMl [lemma, in mathcomp.fingroup.fingroup]
LagrangeMr [lemma, in mathcomp.fingroup.fingroup]
Lagrange_index [lemma, in mathcomp.fingroup.fingroup]
lagrange_gen [lemma, in mathcomp.algebra.qpoly]
lagrange_coords [lemma, in mathcomp.algebra.qpoly]
lagrange_full [lemma, in mathcomp.algebra.qpoly]
lagrange_free [lemma, in mathcomp.algebra.qpoly]
lagrange_sample [lemma, in mathcomp.algebra.qpoly]
lagrange_ [abbreviation, in mathcomp.algebra.qpoly]
lagrange_key [lemma, in mathcomp.algebra.qpoly]
lagrange_def [abbreviation, in mathcomp.algebra.qpoly]
Lagrange.gT [variable, in mathcomp.fingroup.fingroup]
lambda:1033 [binder, in mathcomp.character.character]
lambda:489 [binder, in mathcomp.character.inertia]
lambda:511 [binder, in mathcomp.character.inertia]
lambda:534 [binder, in mathcomp.character.inertia]
large_field_PET [lemma, in mathcomp.field.separable]
last [definition, in mathcomp.ssreflect.seq]
lastI [lemma, in mathcomp.ssreflect.seq]
LastNil [constructor, in mathcomp.ssreflect.seq]
lastP [lemma, in mathcomp.ssreflect.seq]
LastRcons [constructor, in mathcomp.ssreflect.seq]
last_map [lemma, in mathcomp.ssreflect.seq]
last_eq [lemma, in mathcomp.ssreflect.seq]
last_nth [lemma, in mathcomp.ssreflect.seq]
last_ind [lemma, in mathcomp.ssreflect.seq]
last_spec [inductive, in mathcomp.ssreflect.seq]
last_rcons [lemma, in mathcomp.ssreflect.seq]
last_cat [lemma, in mathcomp.ssreflect.seq]
last_cons [lemma, in mathcomp.ssreflect.seq]
last_traject [lemma, in mathcomp.ssreflect.path]
lb_dvd:83 [binder, in mathcomp.ssreflect.prime]
lcmn [definition, in mathcomp.ssreflect.div]
lcmnA [lemma, in mathcomp.ssreflect.div]
lcmnAC [lemma, in mathcomp.ssreflect.div]
lcmnACA [lemma, in mathcomp.ssreflect.div]
lcmnC [lemma, in mathcomp.ssreflect.div]
lcmnCA [lemma, in mathcomp.ssreflect.div]
lcmnMl [lemma, in mathcomp.ssreflect.div]
lcmnMr [lemma, in mathcomp.ssreflect.div]
lcmn_idPl [lemma, in mathcomp.ssreflect.div]
lcmn_idPr [lemma, in mathcomp.ssreflect.div]
lcmn_gt0 [lemma, in mathcomp.ssreflect.div]
lcmn0 [lemma, in mathcomp.ssreflect.div]
lcmn1 [lemma, in mathcomp.ssreflect.div]
lcmz [definition, in mathcomp.algebra.intdiv]
lcmzC [lemma, in mathcomp.algebra.intdiv]
lcmz_neq0 [lemma, in mathcomp.algebra.intdiv]
lcmz_ge0 [lemma, in mathcomp.algebra.intdiv]
lcmz0 [lemma, in mathcomp.algebra.intdiv]
lcm0n [lemma, in mathcomp.ssreflect.div]
lcm0z [lemma, in mathcomp.algebra.intdiv]
lcm1n [lemma, in mathcomp.ssreflect.div]
lcnE [lemma, in mathcomp.solvable.nilpotent]
lcnP [lemma, in mathcomp.solvable.nilpotent]
lcnS [lemma, in mathcomp.solvable.nilpotent]
lcnSn [lemma, in mathcomp.solvable.nilpotent]
lcnSnS [lemma, in mathcomp.solvable.nilpotent]
lcn_neq0 [abbreviation, in mathcomp.field.separable]
lcn_mgFun [definition, in mathcomp.solvable.nilpotent]
lcn_gFun [definition, in mathcomp.solvable.nilpotent]
lcn_igFun [definition, in mathcomp.solvable.nilpotent]
lcn_cont [lemma, in mathcomp.solvable.nilpotent]
lcn_nil_classP [lemma, in mathcomp.solvable.nilpotent]
lcn_bigdprod [lemma, in mathcomp.solvable.nilpotent]
lcn_bigcprod [lemma, in mathcomp.solvable.nilpotent]
lcn_dprod [lemma, in mathcomp.solvable.nilpotent]
lcn_cprod [lemma, in mathcomp.solvable.nilpotent]
lcn_sub_leq [lemma, in mathcomp.solvable.nilpotent]
lcn_central [lemma, in mathcomp.solvable.nilpotent]
lcn_normalS [lemma, in mathcomp.solvable.nilpotent]
lcn_subS [lemma, in mathcomp.solvable.nilpotent]
lcn_norm [lemma, in mathcomp.solvable.nilpotent]
lcn_sub [lemma, in mathcomp.solvable.nilpotent]
lcn_normal [lemma, in mathcomp.solvable.nilpotent]
lcn_char [lemma, in mathcomp.solvable.nilpotent]
lcn_group_set [lemma, in mathcomp.solvable.nilpotent]
lcn0 [lemma, in mathcomp.solvable.nilpotent]
lcn1 [lemma, in mathcomp.solvable.nilpotent]
lcn2 [lemma, in mathcomp.solvable.nilpotent]
Lcorrect [lemma, in mathcomp.solvable.burnside_app]
lcoset [definition, in mathcomp.fingroup.fingroup]
lcosetE [lemma, in mathcomp.fingroup.fingroup]
lcosetK [lemma, in mathcomp.fingroup.fingroup]
lcosetKV [lemma, in mathcomp.fingroup.fingroup]
lcosetM [lemma, in mathcomp.fingroup.fingroup]
lcosetP [lemma, in mathcomp.fingroup.fingroup]
lcosetS [lemma, in mathcomp.fingroup.fingroup]
lcosets [definition, in mathcomp.fingroup.fingroup]
lcosetsP [lemma, in mathcomp.fingroup.fingroup]
lcoset_id [lemma, in mathcomp.fingroup.fingroup]
lcoset_trans [lemma, in mathcomp.fingroup.fingroup]
lcoset_transl [lemma, in mathcomp.fingroup.fingroup]
lcoset_eqP [lemma, in mathcomp.fingroup.fingroup]
lcoset_sym [lemma, in mathcomp.fingroup.fingroup]
lcoset_refl [lemma, in mathcomp.fingroup.fingroup]
lcoset_inj [lemma, in mathcomp.fingroup.fingroup]
lcoset1 [lemma, in mathcomp.fingroup.fingroup]
Ldiv [definition, in mathcomp.solvable.abelian]
LdivJ [lemma, in mathcomp.solvable.abelian]
LdivP [lemma, in mathcomp.solvable.abelian]
LdivT_J [lemma, in mathcomp.solvable.abelian]
lead_coef_poly_XaY [lemma, in mathcomp.algebra.polyXY]
lead_coef_map [lemma, in mathcomp.algebra.poly]
lead_coef_comp [lemma, in mathcomp.algebra.poly]
lead_coef_exp [lemma, in mathcomp.algebra.poly]
lead_coefZ [lemma, in mathcomp.algebra.poly]
lead_coefM [lemma, in mathcomp.algebra.poly]
lead_coef_map_eq [lemma, in mathcomp.algebra.poly]
lead_coef_map_inj [lemma, in mathcomp.algebra.poly]
lead_coef_map_id0 [lemma, in mathcomp.algebra.poly]
lead_coef_lreg [lemma, in mathcomp.algebra.poly]
lead_coef_Mmonic [lemma, in mathcomp.algebra.poly]
lead_coef_monicM [lemma, in mathcomp.algebra.poly]
lead_coefXn [lemma, in mathcomp.algebra.poly]
lead_coefMX [lemma, in mathcomp.algebra.poly]
lead_coefXsubC [lemma, in mathcomp.algebra.poly]
lead_coefX [lemma, in mathcomp.algebra.poly]
lead_coefN [lemma, in mathcomp.algebra.poly]
lead_coef_proper_mul [lemma, in mathcomp.algebra.poly]
lead_coef1 [lemma, in mathcomp.algebra.poly]
lead_coefDr [lemma, in mathcomp.algebra.poly]
lead_coefDl [lemma, in mathcomp.algebra.poly]
lead_coef_eq0 [lemma, in mathcomp.algebra.poly]
lead_coef0 [lemma, in mathcomp.algebra.poly]
lead_coef_poly [lemma, in mathcomp.algebra.poly]
lead_coefC [lemma, in mathcomp.algebra.poly]
lead_coefE [lemma, in mathcomp.algebra.poly]
lead_coef [definition, in mathcomp.algebra.poly]
leBRight_ltBLeft [lemma, in mathcomp.algebra.interval]
leBSide [lemma, in mathcomp.algebra.interval]
leC_nat [definition, in mathcomp.field.algC]
leEmeet:140 [binder, in mathcomp.ssreflect.order]
leEmeet:2525 [binder, in mathcomp.ssreflect.order]
left_trans [lemma, in mathcomp.ssreflect.generic_quotient]
left_arc [lemma, in mathcomp.ssreflect.path]
left_mx_ideal [definition, in mathcomp.algebra.mxalgebra]
lemn:254 [binder, in mathcomp.ssreflect.tuple]
lemn:284 [binder, in mathcomp.ssreflect.tuple]
lemn:289 [binder, in mathcomp.ssreflect.tuple]
lemn:294 [binder, in mathcomp.ssreflect.tuple]
lenm:285 [binder, in mathcomp.ssreflect.tuple]
lenn:276 [binder, in mathcomp.ssreflect.tuple]
lenp:290 [binder, in mathcomp.ssreflect.tuple]
leNz_nat [lemma, in mathcomp.algebra.ssrint]
leP [lemma, in mathcomp.ssreflect.ssrnat]
leq [definition, in mathcomp.ssreflect.ssrnat]
leqDmod [lemma, in mathcomp.ssreflect.div]
leqif [definition, in mathcomp.ssreflect.ssrnat]
leqifP [lemma, in mathcomp.ssreflect.ssrnat]
leqif_mul [lemma, in mathcomp.ssreflect.ssrnat]
leqif_add [lemma, in mathcomp.ssreflect.ssrnat]
leqif_eq [lemma, in mathcomp.ssreflect.ssrnat]
leqif_geq [lemma, in mathcomp.ssreflect.ssrnat]
leqif_trans [lemma, in mathcomp.ssreflect.ssrnat]
leqif_refl [lemma, in mathcomp.ssreflect.ssrnat]
leqif_add_dist [abbreviation, in mathcomp.algebra.ssrint]
leqif_add_distz [abbreviation, in mathcomp.algebra.ssrint]
leqif_sum [lemma, in mathcomp.ssreflect.bigop]
leqLHS [abbreviation, in mathcomp.ssreflect.ssrnat]
leqNgt [lemma, in mathcomp.ssreflect.ssrnat]
leqnn [lemma, in mathcomp.ssreflect.ssrnat]
LeqNotGtn [constructor, in mathcomp.ssreflect.ssrnat]
leqnSn [lemma, in mathcomp.ssreflect.ssrnat]
leqn0 [lemma, in mathcomp.ssreflect.ssrnat]
leqP [lemma, in mathcomp.ssreflect.ssrnat]
leqRHS [abbreviation, in mathcomp.ssreflect.ssrnat]
leqSpred [lemma, in mathcomp.ssreflect.ssrnat]
leqVgt [lemma, in mathcomp.ssreflect.ssrnat]
leqW [lemma, in mathcomp.ssreflect.ssrnat]
leqW_nmono_in [lemma, in mathcomp.ssreflect.ssrnat]
leqW_mono_in [lemma, in mathcomp.ssreflect.ssrnat]
leqW_nmono [lemma, in mathcomp.ssreflect.ssrnat]
leqW_mono [lemma, in mathcomp.ssreflect.ssrnat]
leq_quotient [lemma, in mathcomp.fingroup.quotient]
leq_bin2l [lemma, in mathcomp.ssreflect.binomial]
leq_divLR [lemma, in mathcomp.ssreflect.div]
leq_divDl [lemma, in mathcomp.ssreflect.div]
leq_div2l [lemma, in mathcomp.ssreflect.div]
leq_div2r [lemma, in mathcomp.ssreflect.div]
leq_divRL [lemma, in mathcomp.ssreflect.div]
leq_div [lemma, in mathcomp.ssreflect.div]
leq_mod [lemma, in mathcomp.ssreflect.div]
leq_trunc_div [lemma, in mathcomp.ssreflect.div]
leq_count_subseq [lemma, in mathcomp.ssreflect.seq]
leq_count_mask [lemma, in mathcomp.ssreflect.seq]
leq_rot_add [lemma, in mathcomp.ssreflect.seq]
leq_size_uniq [lemma, in mathcomp.ssreflect.seq]
leq_uniq_count [lemma, in mathcomp.ssreflect.seq]
leq_uniq_countP [lemma, in mathcomp.ssreflect.seq]
leq_fact [lemma, in mathcomp.ssreflect.ssrnat]
leq_pfact [lemma, in mathcomp.ssreflect.ssrnat]
leq_nmono_in [lemma, in mathcomp.ssreflect.ssrnat]
leq_mono_in [lemma, in mathcomp.ssreflect.ssrnat]
leq_nmono [lemma, in mathcomp.ssreflect.ssrnat]
leq_mono [lemma, in mathcomp.ssreflect.ssrnat]
leq_of_leqif [definition, in mathcomp.ssreflect.ssrnat]
leq_sqr [lemma, in mathcomp.ssreflect.ssrnat]
leq_uphalf_double [lemma, in mathcomp.ssreflect.ssrnat]
leq_half_double [lemma, in mathcomp.ssreflect.ssrnat]
leq_Sdouble [lemma, in mathcomp.ssreflect.ssrnat]
leq_double [lemma, in mathcomp.ssreflect.ssrnat]
leq_b1 [lemma, in mathcomp.ssreflect.ssrnat]
leq_exp2r [lemma, in mathcomp.ssreflect.ssrnat]
leq_pexp2l [lemma, in mathcomp.ssreflect.ssrnat]
leq_exp2l [lemma, in mathcomp.ssreflect.ssrnat]
leq_pmul2r [lemma, in mathcomp.ssreflect.ssrnat]
leq_pmul2l [lemma, in mathcomp.ssreflect.ssrnat]
leq_mul [lemma, in mathcomp.ssreflect.ssrnat]
leq_mul2r [lemma, in mathcomp.ssreflect.ssrnat]
leq_mul2l [lemma, in mathcomp.ssreflect.ssrnat]
leq_pmulr [lemma, in mathcomp.ssreflect.ssrnat]
leq_pmull [lemma, in mathcomp.ssreflect.ssrnat]
leq_xor_gtn [inductive, in mathcomp.ssreflect.ssrnat]
leq_min [lemma, in mathcomp.ssreflect.ssrnat]
leq_maxr [lemma, in mathcomp.ssreflect.ssrnat]
leq_maxl [lemma, in mathcomp.ssreflect.ssrnat]
leq_max [lemma, in mathcomp.ssreflect.ssrnat]
leq_sub2lE [lemma, in mathcomp.ssreflect.ssrnat]
leq_sub2rE [lemma, in mathcomp.ssreflect.ssrnat]
leq_subCr [lemma, in mathcomp.ssreflect.ssrnat]
leq_psubCr [lemma, in mathcomp.ssreflect.ssrnat]
leq_subCl [lemma, in mathcomp.ssreflect.ssrnat]
leq_subRL [lemma, in mathcomp.ssreflect.ssrnat]
leq_psubRL [lemma, in mathcomp.ssreflect.ssrnat]
leq_sub [lemma, in mathcomp.ssreflect.ssrnat]
leq_sub2l [lemma, in mathcomp.ssreflect.ssrnat]
leq_sub2r [lemma, in mathcomp.ssreflect.ssrnat]
leq_subrR [lemma, in mathcomp.ssreflect.ssrnat]
leq_subr [lemma, in mathcomp.ssreflect.ssrnat]
leq_subLR [lemma, in mathcomp.ssreflect.ssrnat]
leq_addr [lemma, in mathcomp.ssreflect.ssrnat]
leq_addl [lemma, in mathcomp.ssreflect.ssrnat]
leq_add [lemma, in mathcomp.ssreflect.ssrnat]
leq_add2r [lemma, in mathcomp.ssreflect.ssrnat]
leq_add2l [lemma, in mathcomp.ssreflect.ssrnat]
leq_total [lemma, in mathcomp.ssreflect.ssrnat]
leq_ltn_trans [lemma, in mathcomp.ssreflect.ssrnat]
leq_trans [lemma, in mathcomp.ssreflect.ssrnat]
leq_eqVlt [lemma, in mathcomp.ssreflect.ssrnat]
leq_gtF [lemma, in mathcomp.ssreflect.ssrnat]
leq_pred [lemma, in mathcomp.ssreflect.ssrnat]
leq_card_cover [lemma, in mathcomp.ssreflect.finset]
leq_card_setU [lemma, in mathcomp.ssreflect.finset]
leq_imset_card [lemma, in mathcomp.ssreflect.finset]
leq_add_dist [abbreviation, in mathcomp.algebra.ssrint]
leq_up_log [lemma, in mathcomp.ssreflect.prime]
leq_trunc_log [lemma, in mathcomp.ssreflect.prime]
leq_homg [lemma, in mathcomp.fingroup.morphism]
leq_morphim [lemma, in mathcomp.fingroup.morphism]
leq_ord [lemma, in mathcomp.ssreflect.fintype]
leq_bump2 [lemma, in mathcomp.ssreflect.fintype]
leq_bump [lemma, in mathcomp.ssreflect.fintype]
leq_card [lemma, in mathcomp.ssreflect.fintype]
leq_card_in [lemma, in mathcomp.ssreflect.fintype]
leq_image_card [lemma, in mathcomp.ssreflect.fintype]
leq_sizeP [lemma, in mathcomp.algebra.poly]
leq_bigmax [lemma, in mathcomp.ssreflect.bigop]
leq_bigmax_cond [lemma, in mathcomp.ssreflect.bigop]
leq_bigmax_seq [lemma, in mathcomp.ssreflect.bigop]
leq_prod [lemma, in mathcomp.ssreflect.bigop]
leq_sum [lemma, in mathcomp.ssreflect.bigop]
leq0n [lemma, in mathcomp.ssreflect.ssrnat]
lerq0 [lemma, in mathcomp.algebra.rat]
lerz0 [lemma, in mathcomp.algebra.ssrint]
lerz1 [lemma, in mathcomp.algebra.ssrint]
ler_eexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_niexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_piexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_weexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_wneexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_wpeexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_wniexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_wpiexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_nexpz2r [abbreviation, in mathcomp.algebra.ssrint]
ler_pexpz2r [abbreviation, in mathcomp.algebra.ssrint]
ler_wnexpz2r [abbreviation, in mathcomp.algebra.ssrint]
ler_wpexpz2r [abbreviation, in mathcomp.algebra.ssrint]
ler_wnmulz2r [abbreviation, in mathcomp.algebra.ssrint]
ler_nXz2r [lemma, in mathcomp.algebra.ssrint]
ler_pXz2r [lemma, in mathcomp.algebra.ssrint]
ler_wnXz2r [lemma, in mathcomp.algebra.ssrint]
ler_wpXz2r [lemma, in mathcomp.algebra.ssrint]
ler_eXz2l [lemma, in mathcomp.algebra.ssrint]
ler_niXz2l [lemma, in mathcomp.algebra.ssrint]
ler_piXz2l [lemma, in mathcomp.algebra.ssrint]
ler_weXz2l [lemma, in mathcomp.algebra.ssrint]
ler_wneXz2l [lemma, in mathcomp.algebra.ssrint]
ler_wpeXz2l [lemma, in mathcomp.algebra.ssrint]
ler_wniXz2l [lemma, in mathcomp.algebra.ssrint]
ler_wpiXz2l [lemma, in mathcomp.algebra.ssrint]
ler_nmulz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_nmulz2r [abbreviation, in mathcomp.algebra.ssrint]
ler_wnmulz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_wpmulz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_wpmulz2r [abbreviation, in mathcomp.algebra.ssrint]
ler_pmulz2l [abbreviation, in mathcomp.algebra.ssrint]
ler_pmulz2r [abbreviation, in mathcomp.algebra.ssrint]
ler_int [lemma, in mathcomp.algebra.ssrint]
ler_nMz2l [lemma, in mathcomp.algebra.ssrint]
ler_pMz2l [lemma, in mathcomp.algebra.ssrint]
ler_wnMz2l [lemma, in mathcomp.algebra.ssrint]
ler_wpMz2l [lemma, in mathcomp.algebra.ssrint]
ler_wnMz2r [lemma, in mathcomp.algebra.ssrint]
ler_wpMz2r [lemma, in mathcomp.algebra.ssrint]
ler_nMz2r [lemma, in mathcomp.algebra.ssrint]
ler_pMz2r [lemma, in mathcomp.algebra.ssrint]
ler_def:37 [binder, in mathcomp.algebra.ssrnum]
ler_normD:9 [binder, in mathcomp.algebra.ssrnum]
ler_rat [lemma, in mathcomp.algebra.rat]
ler0q [lemma, in mathcomp.algebra.rat]
ler0z [lemma, in mathcomp.algebra.ssrint]
ler1z [lemma, in mathcomp.algebra.ssrint]
leT':576 [binder, in mathcomp.ssreflect.path]
leT':582 [binder, in mathcomp.ssreflect.path]
leT':589 [binder, in mathcomp.ssreflect.path]
leT':670 [binder, in mathcomp.ssreflect.path]
leT':681 [binder, in mathcomp.ssreflect.path]
leT:128 [binder, in mathcomp.ssreflect.ssrbool]
leT:237 [binder, in mathcomp.ssreflect.path]
leT:241 [binder, in mathcomp.ssreflect.path]
leT:518 [binder, in mathcomp.ssreflect.path]
leT:540 [binder, in mathcomp.ssreflect.path]
leT:547 [binder, in mathcomp.ssreflect.path]
leT:552 [binder, in mathcomp.ssreflect.path]
leT:555 [binder, in mathcomp.ssreflect.path]
leT:575 [binder, in mathcomp.ssreflect.path]
leT:581 [binder, in mathcomp.ssreflect.path]
leT:588 [binder, in mathcomp.ssreflect.path]
leT:594 [binder, in mathcomp.ssreflect.path]
leT:601 [binder, in mathcomp.ssreflect.path]
leT:652 [binder, in mathcomp.ssreflect.path]
leT:656 [binder, in mathcomp.ssreflect.path]
leT:659 [binder, in mathcomp.ssreflect.path]
leT:663 [binder, in mathcomp.ssreflect.path]
leT:669 [binder, in mathcomp.ssreflect.path]
leT:680 [binder, in mathcomp.ssreflect.path]
lex1:224 [binder, in mathcomp.ssreflect.order]
lezD1 [lemma, in mathcomp.algebra.ssrint]
lezN_nat [lemma, in mathcomp.algebra.ssrint]
lez_divLR [lemma, in mathcomp.algebra.intdiv]
lez_pdiv2r [lemma, in mathcomp.algebra.intdiv]
lez_divRL [lemma, in mathcomp.algebra.intdiv]
lez_div [lemma, in mathcomp.algebra.intdiv]
lez_floor [lemma, in mathcomp.algebra.intdiv]
lez_abs [lemma, in mathcomp.algebra.ssrint]
lez_addr1 [abbreviation, in mathcomp.algebra.ssrint]
lez_add1r [abbreviation, in mathcomp.algebra.ssrint]
lez_nat [lemma, in mathcomp.algebra.ssrint]
lez0_abs [lemma, in mathcomp.algebra.ssrint]
lez0_nat [lemma, in mathcomp.algebra.ssrint]
lez1D [lemma, in mathcomp.algebra.ssrint]
le_ninfty [lemma, in mathcomp.algebra.interval]
le_bound_trans [lemma, in mathcomp.algebra.interval]
le_bound_anti [lemma, in mathcomp.algebra.interval]
le_bound_refl [lemma, in mathcomp.algebra.interval]
le_bound [definition, in mathcomp.algebra.interval]
le_x:2741 [binder, in mathcomp.ssreflect.seq]
le_mn2:159 [binder, in mathcomp.ssreflect.ssrnat]
le_mn1:158 [binder, in mathcomp.ssreflect.ssrnat]
le_irrelevance [lemma, in mathcomp.ssreflect.ssrnat]
le_fix_order [lemma, in mathcomp.ssreflect.finset]
le_mn:1791 [binder, in mathcomp.algebra.matrix]
le_mn:1788 [binder, in mathcomp.algebra.matrix]
le_ij:450 [binder, in mathcomp.field.closed_field]
le_def:2675 [binder, in mathcomp.ssreflect.order]
le_total:2650 [binder, in mathcomp.ssreflect.order]
le_trans:2649 [binder, in mathcomp.ssreflect.order]
le_anti:2648 [binder, in mathcomp.ssreflect.order]
le_def:2575 [binder, in mathcomp.ssreflect.order]
le_total:2548 [binder, in mathcomp.ssreflect.order]
le_total:2535 [binder, in mathcomp.ssreflect.order]
le_total:328 [binder, in mathcomp.ssreflect.order]
le_xy:71 [binder, in mathcomp.ssreflect.order]
le_def:35 [binder, in mathcomp.ssreflect.order]
le_trans:22 [binder, in mathcomp.ssreflect.order]
le_anti:21 [binder, in mathcomp.ssreflect.order]
le_refl:20 [binder, in mathcomp.ssreflect.order]
le_trans:10 [binder, in mathcomp.ssreflect.order]
le_anti:9 [binder, in mathcomp.ssreflect.order]
le_refl:8 [binder, in mathcomp.ssreflect.order]
le_def:2612 [binder, in mathcomp.algebra.ssrnum]
le_def:2523 [binder, in mathcomp.algebra.ssrnum]
le_rat_total [lemma, in mathcomp.algebra.rat]
le_rat0_anti [lemma, in mathcomp.algebra.rat]
le_rat0M [lemma, in mathcomp.algebra.rat]
le_rat0D [lemma, in mathcomp.algebra.rat]
le_rat0 [lemma, in mathcomp.algebra.rat]
le_ratE [lemma, in mathcomp.algebra.rat]
le_rat [definition, in mathcomp.algebra.rat]
le_n_m:860 [binder, in mathcomp.ssreflect.fintype]
le_big_ord_cond [lemma, in mathcomp.ssreflect.bigop]
le_big_nat [lemma, in mathcomp.ssreflect.bigop]
le_big_nat_cond [lemma, in mathcomp.ssreflect.bigop]
le_big_ord [lemma, in mathcomp.ssreflect.bigop]
le_n12:990 [binder, in mathcomp.ssreflect.bigop]
le_n12:979 [binder, in mathcomp.ssreflect.bigop]
le_n12:968 [binder, in mathcomp.ssreflect.bigop]
le_n12:956 [binder, in mathcomp.ssreflect.bigop]
le0x:169 [binder, in mathcomp.ssreflect.order]
le0z_nat [lemma, in mathcomp.algebra.ssrint]
le0_total:2565 [binder, in mathcomp.algebra.ssrnum]
le0_anti:2560 [binder, in mathcomp.algebra.ssrnum]
le0_mul:2558 [binder, in mathcomp.algebra.ssrnum]
le0_add:2555 [binder, in mathcomp.algebra.ssrnum]
le:19 [binder, in mathcomp.ssreflect.order]
le:2569 [binder, in mathcomp.ssreflect.order]
le:2635 [binder, in mathcomp.ssreflect.order]
le:2669 [binder, in mathcomp.ssreflect.order]
le:3 [binder, in mathcomp.ssreflect.order]
le:31 [binder, in mathcomp.ssreflect.order]
LfunAlgebra [section, in mathcomp.algebra.vector]
LfunAlgebra.R [variable, in mathcomp.algebra.vector]
LfunAlgebra.vT [variable, in mathcomp.algebra.vector]
LfunAlgebra.vT_proper [variable, in mathcomp.algebra.vector]
LfunDefs [section, in mathcomp.algebra.vector]
LfunDefs.R [variable, in mathcomp.algebra.vector]
lfunE [lemma, in mathcomp.algebra.vector]
lfunP [lemma, in mathcomp.algebra.vector]
lfunPn [lemma, in mathcomp.algebra.vector]
LfunVectType [section, in mathcomp.algebra.vector]
LfunVectType.aT [variable, in mathcomp.algebra.vector]
LfunVectType.R [variable, in mathcomp.algebra.vector]
LfunVectType.rT [variable, in mathcomp.algebra.vector]
_ *:l _ [notation, in mathcomp.algebra.vector]
LfunVspaceDefs [section, in mathcomp.algebra.vector]
LfunVspaceDefs.K [variable, in mathcomp.algebra.vector]
LfunZmodType [section, in mathcomp.algebra.vector]
LfunZmodType.aT [variable, in mathcomp.algebra.vector]
LfunZmodType.hb_instance_70.f [variable, in mathcomp.algebra.vector]
LfunZmodType.hb_instance_70 [section, in mathcomp.algebra.vector]
LfunZmodType.R [variable, in mathcomp.algebra.vector]
LfunZmodType.rT [variable, in mathcomp.algebra.vector]
lfun_algType [definition, in mathcomp.algebra.vector]
lfun_algMixin [definition, in mathcomp.algebra.vector]
lfun_lalgType [definition, in mathcomp.algebra.vector]
lfun_lalgMixin [definition, in mathcomp.algebra.vector]
lfun_ringType [definition, in mathcomp.algebra.vector]
lfun_comp_ringType [definition, in mathcomp.algebra.vector]
lfun_comp_ringMixin [definition, in mathcomp.algebra.vector]
lfun_simp [definition, in mathcomp.algebra.vector]
lfun_vect_iso [lemma, in mathcomp.algebra.vector]
lfun_scaleDl [lemma, in mathcomp.algebra.vector]
lfun_scaleDr [lemma, in mathcomp.algebra.vector]
lfun_scale1 [lemma, in mathcomp.algebra.vector]
lfun_scaleA [lemma, in mathcomp.algebra.vector]
lfun_addN [lemma, in mathcomp.algebra.vector]
lfun_add0 [lemma, in mathcomp.algebra.vector]
lfun_addC [lemma, in mathcomp.algebra.vector]
lfun_addA [lemma, in mathcomp.algebra.vector]
lfun_is_linear [lemma, in mathcomp.algebra.vector]
lfun_preim [definition, in mathcomp.algebra.vector]
lfun_img_unlockable [definition, in mathcomp.algebra.vector]
lfun_img [definition, in mathcomp.algebra.vector]
lfun_img_def [definition, in mathcomp.algebra.vector]
lfun_img_key [lemma, in mathcomp.algebra.vector]
lfun_key [lemma, in mathcomp.algebra.vector]
lfun1_neq0 [lemma, in mathcomp.algebra.vector]
lfun1_poly [lemma, in mathcomp.field.falgebra]
lhs:106 [binder, in mathcomp.ssreflect.choice]
lhs:99 [binder, in mathcomp.ssreflect.choice]
lid:101 [binder, in mathcomp.ssreflect.ssrAC]
lift [definition, in mathcomp.ssreflect.fintype]
liftK [lemma, in mathcomp.ssreflect.fintype]
LiftPerm [section, in mathcomp.fingroup.perm]
LiftPerm.n [variable, in mathcomp.fingroup.perm]
lift_permV [lemma, in mathcomp.fingroup.perm]
lift_perm1 [lemma, in mathcomp.fingroup.perm]
lift_permM [lemma, in mathcomp.fingroup.perm]
lift_perm_lift [lemma, in mathcomp.fingroup.perm]
lift_perm_id [lemma, in mathcomp.fingroup.perm]
lift_perm [definition, in mathcomp.fingroup.perm]
lift_permK [lemma, in mathcomp.fingroup.perm]
lift_perm_fun [definition, in mathcomp.fingroup.perm]
lift_embed [abbreviation, in mathcomp.ssreflect.generic_quotient]
lift_cst [abbreviation, in mathcomp.ssreflect.generic_quotient]
lift_op11 [abbreviation, in mathcomp.ssreflect.generic_quotient]
lift_fun2 [abbreviation, in mathcomp.ssreflect.generic_quotient]
lift_fun1 [abbreviation, in mathcomp.ssreflect.generic_quotient]
lift_op2 [abbreviation, in mathcomp.ssreflect.generic_quotient]
lift_op1 [abbreviation, in mathcomp.ssreflect.generic_quotient]
lift_max [lemma, in mathcomp.ssreflect.fintype]
lift_inj [lemma, in mathcomp.ssreflect.fintype]
lift_eqF [lemma, in mathcomp.ssreflect.fintype]
lift_subproof [lemma, in mathcomp.ssreflect.fintype]
lift0 [lemma, in mathcomp.ssreflect.fintype]
lift0_mx_is_perm [lemma, in mathcomp.algebra.matrix]
lift0_mx_perm [lemma, in mathcomp.algebra.matrix]
lift0_mx [definition, in mathcomp.algebra.matrix]
lift0_perm_eq0 [lemma, in mathcomp.algebra.matrix]
lift0_permK [lemma, in mathcomp.algebra.matrix]
lift0_perm_lift [lemma, in mathcomp.algebra.matrix]
lift0_perm0 [lemma, in mathcomp.algebra.matrix]
lift0_perm [definition, in mathcomp.algebra.matrix]
limg [abbreviation, in mathcomp.algebra.vector]
limgD [lemma, in mathcomp.algebra.vector]
limgS [lemma, in mathcomp.algebra.vector]
limg_gal [lemma, in mathcomp.field.galois]
limg_proj [lemma, in mathcomp.algebra.vector]
limg_comp [lemma, in mathcomp.algebra.vector]
limg_ker0 [lemma, in mathcomp.algebra.vector]
limg_basis_of [lemma, in mathcomp.algebra.vector]
limg_dim_eq [lemma, in mathcomp.algebra.vector]
limg_ker_dim [lemma, in mathcomp.algebra.vector]
limg_ker_compl [lemma, in mathcomp.algebra.vector]
limg_lfunVK [lemma, in mathcomp.algebra.vector]
limg_span [lemma, in mathcomp.algebra.vector]
limg_bigcap [lemma, in mathcomp.algebra.vector]
limg_cap [lemma, in mathcomp.algebra.vector]
limg_sum [lemma, in mathcomp.algebra.vector]
limg_line [lemma, in mathcomp.algebra.vector]
limg_amulr [lemma, in mathcomp.field.falgebra]
limg0 [lemma, in mathcomp.algebra.vector]
lim0g [lemma, in mathcomp.algebra.vector]
lim1g [lemma, in mathcomp.algebra.vector]
LinAut [section, in mathcomp.algebra.vector]
LinAut.f [variable, in mathcomp.algebra.vector]
LinAut.K [variable, in mathcomp.algebra.vector]
LinAut.kerf0 [variable, in mathcomp.algebra.vector]
LinAut.vT [variable, in mathcomp.algebra.vector]
Linear [section, in mathcomp.algebra.rat]
Linear [section, in mathcomp.character.character]
LinearImage [section, in mathcomp.algebra.vector]
LinearImageComp [section, in mathcomp.algebra.vector]
LinearImageComp.aT [variable, in mathcomp.algebra.vector]
LinearImageComp.K [variable, in mathcomp.algebra.vector]
LinearImageComp.rT [variable, in mathcomp.algebra.vector]
LinearImageComp.vT [variable, in mathcomp.algebra.vector]
LinearImage.aT [variable, in mathcomp.algebra.vector]
LinearImage.K [variable, in mathcomp.algebra.vector]
LinearImage.rT [variable, in mathcomp.algebra.vector]
linearMn [lemma, in mathcomp.algebra.ssrint]
LinearPreimage [section, in mathcomp.algebra.vector]
LinearPreimage.aT [variable, in mathcomp.algebra.vector]
LinearPreimage.K [variable, in mathcomp.algebra.vector]
LinearPreimage.rT [variable, in mathcomp.algebra.vector]
linear_irr_comp [lemma, in mathcomp.character.mxrepresentation]
linear_irr [definition, in mathcomp.character.mxrepresentation]
linear_mxsimple [lemma, in mathcomp.character.mxrepresentation]
linear_mx_abs_irr [lemma, in mathcomp.character.mxrepresentation]
linear_subproof:1107 [binder, in mathcomp.algebra.ssralg]
linear_subproof:1069 [binder, in mathcomp.algebra.ssralg]
linear_of_free [lemma, in mathcomp.algebra.vector]
linear_char_divr [lemma, in mathcomp.character.character]
linear_char [definition, in mathcomp.character.character]
linear_char_pred [definition, in mathcomp.character.character]
Linear.G [variable, in mathcomp.character.character]
Linear.gT [variable, in mathcomp.character.character]
Linear.OneChar [section, in mathcomp.character.character]
Linear.OneChar.CFxi [variable, in mathcomp.character.character]
Linear.OneChar.xi [variable, in mathcomp.character.character]
Linear.OneChar.xiMV [variable, in mathcomp.character.character]
linfun [definition, in mathcomp.algebra.vector]
linfun_unlockable [definition, in mathcomp.algebra.vector]
linfun_def [definition, in mathcomp.algebra.vector]
linfun_ahom [definition, in mathcomp.field.falgebra]
linfun_is_ahom [lemma, in mathcomp.field.falgebra]
linG:933 [binder, in mathcomp.character.character]
lin_mul_row_is_linear [lemma, in mathcomp.algebra.matrix]
lin_mul_row [definition, in mathcomp.algebra.matrix]
lin_mulmx_is_linear [lemma, in mathcomp.algebra.matrix]
lin_mulmx [definition, in mathcomp.algebra.matrix]
lin_mulmxr_is_linear [lemma, in mathcomp.algebra.matrix]
lin_mulmxr [definition, in mathcomp.algebra.matrix]
lin_mx [definition, in mathcomp.algebra.matrix]
lin_char_group [lemma, in mathcomp.character.character]
lin_irr_der1 [lemma, in mathcomp.character.character]
lin_Res_IirrE [lemma, in mathcomp.character.character]
lin_char_der1 [lemma, in mathcomp.character.character]
lin_char_unitr [lemma, in mathcomp.character.character]
lin_char_irr [lemma, in mathcomp.character.character]
lin_charV_conj [lemma, in mathcomp.character.character]
lin_char_unity_root [lemma, in mathcomp.character.character]
lin_charX [lemma, in mathcomp.character.character]
lin_charV [lemma, in mathcomp.character.character]
lin_char_neq0 [lemma, in mathcomp.character.character]
lin_char_prod [lemma, in mathcomp.character.character]
lin_charM [lemma, in mathcomp.character.character]
lin_charW [lemma, in mathcomp.character.character]
lin_char1 [lemma, in mathcomp.character.character]
lin1_mx [definition, in mathcomp.algebra.matrix]
lin1_mx_key [lemma, in mathcomp.algebra.matrix]
li0:4800 [binder, in mathcomp.ssreflect.order]
lj:4801 [binder, in mathcomp.ssreflect.order]
lker [definition, in mathcomp.algebra.vector]
lkerE [lemma, in mathcomp.algebra.vector]
lker_proj [lemma, in mathcomp.algebra.vector]
lker0P [lemma, in mathcomp.algebra.vector]
lker0_compfVK [lemma, in mathcomp.algebra.vector]
lker0_compfK [lemma, in mathcomp.algebra.vector]
lker0_compKf [lemma, in mathcomp.algebra.vector]
lker0_compVKf [lemma, in mathcomp.algebra.vector]
lker0_compfV [lemma, in mathcomp.algebra.vector]
lker0_lfunVK [lemma, in mathcomp.algebra.vector]
lker0_limgf [lemma, in mathcomp.algebra.vector]
lker0_compVf [lemma, in mathcomp.algebra.vector]
lker0_lfunK [lemma, in mathcomp.algebra.vector]
lker0_amulr [lemma, in mathcomp.field.falgebra]
lker0_amull [lemma, in mathcomp.field.falgebra]
LMod [section, in mathcomp.algebra.ssrint]
Lmodule_hasFinDim.Exports [module, in mathcomp.algebra.vector]
Lmodule_hasFinDim.identity_builder [definition, in mathcomp.algebra.vector]
Lmodule_hasFinDim.phant_axioms [definition, in mathcomp.algebra.vector]
Lmodule_hasFinDim.phant_Build [definition, in mathcomp.algebra.vector]
Lmodule_hasFinDim.vector_subdef [projection, in mathcomp.algebra.vector]
Lmodule_hasFinDim.dim [projection, in mathcomp.algebra.vector]
Lmodule_hasFinDim.axioms_ [record, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim_V__canonical__GRing_Lmodule [definition, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim.local_mixin_GRing_Zmodule_isLmodule [variable, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim_V__canonical__GRing_Zmodule [definition, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim.local_mixin_GRing_Nmodule_isZmodule [variable, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim_V__canonical__GRing_Nmodule [definition, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim_V__canonical__choice_Choice [definition, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim_V__canonical__eqtype_Equality [definition, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim.local_mixin_eqtype_hasDecEq [variable, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim.local_mixin_choice_hasChoice [variable, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim.local_mixin_GRing_isNmodule [variable, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim.V [variable, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim.R [variable, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Lmodule_hasFinDim [section, in mathcomp.algebra.vector]
Lmodule_hasFinDim [module, in mathcomp.algebra.vector]
LMod.R [variable, in mathcomp.algebra.ssrint]
LMod.V [variable, in mathcomp.algebra.ssrint]
logn [definition, in mathcomp.ssreflect.prime]
lognE [lemma, in mathcomp.ssreflect.prime]
lognM [lemma, in mathcomp.ssreflect.prime]
lognSg [lemma, in mathcomp.fingroup.fingroup]
lognX [lemma, in mathcomp.ssreflect.prime]
logn_morphim [lemma, in mathcomp.fingroup.quotient]
logn_fact [lemma, in mathcomp.ssreflect.binomial]
logn_quotient_cent_cyclic_pgroup [lemma, in mathcomp.solvable.pgroup]
logn_lcm [lemma, in mathcomp.ssreflect.prime]
logn_gcd [lemma, in mathcomp.ssreflect.prime]
logn_part [lemma, in mathcomp.ssreflect.prime]
logn_count_dvd [lemma, in mathcomp.ssreflect.prime]
logn_div [lemma, in mathcomp.ssreflect.prime]
logn_coprime [lemma, in mathcomp.ssreflect.prime]
logn_Gauss [lemma, in mathcomp.ssreflect.prime]
logn_prime [lemma, in mathcomp.ssreflect.prime]
logn_gt0 [lemma, in mathcomp.ssreflect.prime]
logn_rec [definition, in mathcomp.ssreflect.prime]
logn_quotient [lemma, in mathcomp.solvable.abelian]
logn_le_p_rank [lemma, in mathcomp.solvable.abelian]
logn_card_GL_p [lemma, in mathcomp.algebra.mxalgebra]
logn0 [lemma, in mathcomp.ssreflect.prime]
logn1 [lemma, in mathcomp.ssreflect.prime]
lone_subgroup_char [lemma, in mathcomp.fingroup.automorphism]
looping [definition, in mathcomp.ssreflect.path]
loopingP [lemma, in mathcomp.ssreflect.path]
looping_uniq [lemma, in mathcomp.ssreflect.path]
looping_order [lemma, in mathcomp.ssreflect.fingraph]
loop:1625 [binder, in mathcomp.algebra.ssralg]
loop:265 [binder, in mathcomp.ssreflect.prime]
loop:2768 [binder, in mathcomp.ssreflect.seq]
loop:492 [binder, in mathcomp.ssreflect.ssrnat]
loop:497 [binder, in mathcomp.algebra.polydiv]
loop:499 [binder, in mathcomp.ssreflect.ssrnat]
loop:70 [binder, in mathcomp.algebra.polydiv]
LowerCentral [section, in mathcomp.solvable.nilpotent]
LowerCentral.gT [variable, in mathcomp.solvable.nilpotent]
lower_central_at_group [definition, in mathcomp.solvable.nilpotent]
lower_central_at [definition, in mathcomp.solvable.nilpotent]
lower_central_at_rec [definition, in mathcomp.solvable.nilpotent]
lpreimK [lemma, in mathcomp.algebra.vector]
lpreimS [lemma, in mathcomp.algebra.vector]
lpreim_cap_limg [lemma, in mathcomp.algebra.vector]
lpreim0 [lemma, in mathcomp.algebra.vector]
lq:174 [binder, in mathcomp.field.closed_field]
lreg_polyZ_eq0 [lemma, in mathcomp.algebra.poly]
lreg_size [lemma, in mathcomp.algebra.poly]
lreg_lead0 [lemma, in mathcomp.algebra.poly]
lreg_lead [lemma, in mathcomp.algebra.poly]
lr:130 [binder, in mathcomp.field.closed_field]
lshift [definition, in mathcomp.ssreflect.fintype]
lshift_inj [lemma, in mathcomp.ssreflect.fintype]
lshift_subproof [lemma, in mathcomp.ssreflect.fintype]
lshift0 [lemma, in mathcomp.algebra.zmodp]
lsubmx [definition, in mathcomp.algebra.matrix]
lsubmxEsub [lemma, in mathcomp.algebra.matrix]
lsubmx_key [lemma, in mathcomp.algebra.matrix]
ltBRight_leBLeft [lemma, in mathcomp.algebra.interval]
ltBSide [lemma, in mathcomp.algebra.interval]
ltC_nat [definition, in mathcomp.field.algC]
lteBSide [definition, in mathcomp.algebra.interval]
lteif_in_itv [lemma, in mathcomp.algebra.interval]
lteNz_nat [definition, in mathcomp.algebra.ssrint]
ltezN_nat [definition, in mathcomp.algebra.ssrint]
ltez_natE [definition, in mathcomp.algebra.ssrint]
ltez_nat [definition, in mathcomp.algebra.ssrint]
ltmx [definition, in mathcomp.algebra.mxalgebra]
ltmxE [lemma, in mathcomp.algebra.mxalgebra]
ltmxEneq [lemma, in mathcomp.algebra.mxalgebra]
ltmxErank [lemma, in mathcomp.algebra.mxalgebra]
LtmxIdentities [section, in mathcomp.algebra.mxalgebra]
LtmxIdentities.A [variable, in mathcomp.algebra.mxalgebra]
LtmxIdentities.B [variable, in mathcomp.algebra.mxalgebra]
LtmxIdentities.F [variable, in mathcomp.algebra.mxalgebra]
LtmxIdentities.m1 [variable, in mathcomp.algebra.mxalgebra]
LtmxIdentities.m2 [variable, in mathcomp.algebra.mxalgebra]
LtmxIdentities.n [variable, in mathcomp.algebra.mxalgebra]
'M_ _ (type_scope) [notation, in mathcomp.algebra.mxalgebra]
'M_ ( _ , _ ) (type_scope) [notation, in mathcomp.algebra.mxalgebra]
ltmxW [lemma, in mathcomp.algebra.mxalgebra]
ltmx_irrefl [lemma, in mathcomp.algebra.mxalgebra]
ltmx_trans [lemma, in mathcomp.algebra.mxalgebra]
ltmx_sub_trans [lemma, in mathcomp.algebra.mxalgebra]
ltmx0 [lemma, in mathcomp.algebra.mxalgebra]
ltmx1 [lemma, in mathcomp.algebra.mxalgebra]
ltn [definition, in mathcomp.ssreflect.ssrnat]
ltngtP [lemma, in mathcomp.ssreflect.ssrnat]
ltnLHS [abbreviation, in mathcomp.ssreflect.ssrnat]
ltnn [lemma, in mathcomp.ssreflect.ssrnat]
ltnNge [lemma, in mathcomp.ssreflect.ssrnat]
ltnNleqif [lemma, in mathcomp.ssreflect.ssrnat]
LtnNotGeq [constructor, in mathcomp.ssreflect.ssrnat]
ltnP [lemma, in mathcomp.ssreflect.ssrnat]
ltnRHS [abbreviation, in mathcomp.ssreflect.ssrnat]
ltnS [lemma, in mathcomp.ssreflect.ssrnat]
ltnSE [lemma, in mathcomp.ssreflect.ssrnat]
ltnSn [lemma, in mathcomp.ssreflect.ssrnat]
ltnW [lemma, in mathcomp.ssreflect.ssrnat]
ltnW_nhomo_in [lemma, in mathcomp.ssreflect.ssrnat]
ltnW_homo_in [lemma, in mathcomp.ssreflect.ssrnat]
ltnW_nhomo [lemma, in mathcomp.ssreflect.ssrnat]
ltnW_homo [lemma, in mathcomp.ssreflect.ssrnat]
ltNz_nat [lemma, in mathcomp.algebra.ssrint]
ltn_quotient [lemma, in mathcomp.fingroup.quotient]
ltn_divRL [lemma, in mathcomp.ssreflect.div]
ltn_Pdiv [lemma, in mathcomp.ssreflect.div]
ltn_divLR [lemma, in mathcomp.ssreflect.div]
ltn_ceil [lemma, in mathcomp.ssreflect.div]
ltn_pmod [lemma, in mathcomp.ssreflect.div]
ltn_mod [lemma, in mathcomp.ssreflect.div]
ltn_size_undup [lemma, in mathcomp.ssreflect.seq]
ltn_pfact [lemma, in mathcomp.ssreflect.ssrnat]
ltn_leqif [lemma, in mathcomp.ssreflect.ssrnat]
ltn_sqr [lemma, in mathcomp.ssreflect.ssrnat]
ltn_uphalf_double [lemma, in mathcomp.ssreflect.ssrnat]
ltn_half_double [lemma, in mathcomp.ssreflect.ssrnat]
ltn_Sdouble [lemma, in mathcomp.ssreflect.ssrnat]
ltn_double [lemma, in mathcomp.ssreflect.ssrnat]
ltn_fact [lemma, in mathcomp.ssreflect.ssrnat]
ltn_exp2r [lemma, in mathcomp.ssreflect.ssrnat]
ltn_pexp2l [lemma, in mathcomp.ssreflect.ssrnat]
ltn_exp2l [lemma, in mathcomp.ssreflect.ssrnat]
ltn_expl [lemma, in mathcomp.ssreflect.ssrnat]
ltn_mul [lemma, in mathcomp.ssreflect.ssrnat]
ltn_Pmulr [lemma, in mathcomp.ssreflect.ssrnat]
ltn_Pmull [lemma, in mathcomp.ssreflect.ssrnat]
ltn_pmul2r [lemma, in mathcomp.ssreflect.ssrnat]
ltn_pmul2l [lemma, in mathcomp.ssreflect.ssrnat]
ltn_mul2r [lemma, in mathcomp.ssreflect.ssrnat]
ltn_mul2l [lemma, in mathcomp.ssreflect.ssrnat]
ltn_xor_geq [inductive, in mathcomp.ssreflect.ssrnat]
ltn_min [lemma, in mathcomp.ssreflect.ssrnat]
ltn_sub2lE [lemma, in mathcomp.ssreflect.ssrnat]
ltn_sub2rE [lemma, in mathcomp.ssreflect.ssrnat]
ltn_subCl [lemma, in mathcomp.ssreflect.ssrnat]
ltn_psubCl [lemma, in mathcomp.ssreflect.ssrnat]
ltn_subCr [lemma, in mathcomp.ssreflect.ssrnat]
ltn_subLR [lemma, in mathcomp.ssreflect.ssrnat]
ltn_psubLR [lemma, in mathcomp.ssreflect.ssrnat]
ltn_subRL [lemma, in mathcomp.ssreflect.ssrnat]
ltn_sub2l [lemma, in mathcomp.ssreflect.ssrnat]
ltn_sub2r [lemma, in mathcomp.ssreflect.ssrnat]
ltn_subrL [lemma, in mathcomp.ssreflect.ssrnat]
ltn_subrR [lemma, in mathcomp.ssreflect.ssrnat]
ltn_addr [lemma, in mathcomp.ssreflect.ssrnat]
ltn_addl [lemma, in mathcomp.ssreflect.ssrnat]
ltn_add2r [lemma, in mathcomp.ssreflect.ssrnat]
ltn_add2l [lemma, in mathcomp.ssreflect.ssrnat]
ltn_ind [lemma, in mathcomp.ssreflect.ssrnat]
ltn_trans [lemma, in mathcomp.ssreflect.ssrnat]
ltn_neqAle [lemma, in mathcomp.ssreflect.ssrnat]
ltn_geF [lemma, in mathcomp.ssreflect.ssrnat]
ltn_eqF [lemma, in mathcomp.ssreflect.ssrnat]
ltn_predK [lemma, in mathcomp.ssreflect.ssrnat]
ltn_predRL [lemma, in mathcomp.ssreflect.ssrnat]
ltn_predL [lemma, in mathcomp.ssreflect.ssrnat]
ltn_log_quotient [lemma, in mathcomp.solvable.pgroup]
ltn_sorted_uniq_leq [lemma, in mathcomp.ssreflect.path]
ltn_odd_Frobenius_ker [lemma, in mathcomp.solvable.frobenius]
ltn_logl [lemma, in mathcomp.ssreflect.prime]
ltn_log0 [lemma, in mathcomp.ssreflect.prime]
ltn_pdiv2_prime [lemma, in mathcomp.ssreflect.prime]
ltn_morphim [lemma, in mathcomp.fingroup.morphism]
ltn_unsplit [lemma, in mathcomp.ssreflect.fintype]
ltn_ord [lemma, in mathcomp.ssreflect.fintype]
ltn0 [lemma, in mathcomp.ssreflect.ssrnat]
ltn0Sn [lemma, in mathcomp.ssreflect.ssrnat]
LtoC:66 [binder, in mathcomp.field.algebraics_fundamentals]
ltP [lemma, in mathcomp.ssreflect.ssrnat]
ltrq0 [lemma, in mathcomp.algebra.rat]
ltrz0 [lemma, in mathcomp.algebra.ssrint]
ltrz1 [lemma, in mathcomp.algebra.ssrint]
ltr_eexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ltr_niexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ltr_piexpz2l [abbreviation, in mathcomp.algebra.ssrint]
ltr_nexpz2r [abbreviation, in mathcomp.algebra.ssrint]
ltr_pexpz2r [abbreviation, in mathcomp.algebra.ssrint]
ltr_nXz2r [lemma, in mathcomp.algebra.ssrint]
ltr_pXz2r [lemma, in mathcomp.algebra.ssrint]
ltr_eXz2l [lemma, in mathcomp.algebra.ssrint]
ltr_niXz2l [lemma, in mathcomp.algebra.ssrint]
ltr_piXz2l [lemma, in mathcomp.algebra.ssrint]
ltr_nmulz2l [abbreviation, in mathcomp.algebra.ssrint]
ltr_nmulz2r [abbreviation, in mathcomp.algebra.ssrint]
ltr_pmulz2l [abbreviation, in mathcomp.algebra.ssrint]
ltr_pmulz2r [abbreviation, in mathcomp.algebra.ssrint]
ltr_int [lemma, in mathcomp.algebra.ssrint]
ltr_nMz2l [lemma, in mathcomp.algebra.ssrint]
ltr_pMz2l [lemma, in mathcomp.algebra.ssrint]
ltr_nMz2r [lemma, in mathcomp.algebra.ssrint]
ltr_pMz2r [lemma, in mathcomp.algebra.ssrint]
ltr_rat [lemma, in mathcomp.algebra.rat]
ltr0q [lemma, in mathcomp.algebra.rat]
ltr0z [lemma, in mathcomp.algebra.ssrint]
ltr0_sgz [lemma, in mathcomp.algebra.ssrint]
ltr1z [lemma, in mathcomp.algebra.ssrint]
ltzD1 [lemma, in mathcomp.algebra.ssrint]
ltzN_nat [lemma, in mathcomp.algebra.ssrint]
ltz_divRL [lemma, in mathcomp.algebra.intdiv]
ltz_divLR [lemma, in mathcomp.algebra.intdiv]
ltz_ceil [lemma, in mathcomp.algebra.intdiv]
ltz_mod [lemma, in mathcomp.algebra.intdiv]
ltz_pmod [lemma, in mathcomp.algebra.intdiv]
ltz_addr1 [abbreviation, in mathcomp.algebra.ssrint]
ltz_add1r [abbreviation, in mathcomp.algebra.ssrint]
ltz_nat [lemma, in mathcomp.algebra.ssrint]
ltz0_abs [lemma, in mathcomp.algebra.ssrint]
ltz1D [lemma, in mathcomp.algebra.ssrint]
lt_in_itv [lemma, in mathcomp.algebra.interval]
lt_ninfty [lemma, in mathcomp.algebra.interval]
lt_bound_def [lemma, in mathcomp.algebra.interval]
lt_bound [definition, in mathcomp.algebra.interval]
lt_mn2:165 [binder, in mathcomp.ssreflect.ssrnat]
lt_mn1:164 [binder, in mathcomp.ssreflect.ssrnat]
lt_irrelevance [lemma, in mathcomp.ssreflect.ssrnat]
lt_total:2686 [binder, in mathcomp.ssreflect.order]
lt_trans:2683 [binder, in mathcomp.ssreflect.order]
lt_irr:2682 [binder, in mathcomp.ssreflect.order]
lt_def:2641 [binder, in mathcomp.ssreflect.order]
lt_def:2578 [binder, in mathcomp.ssreflect.order]
lt_trans:50 [binder, in mathcomp.ssreflect.order]
lt_irr:49 [binder, in mathcomp.ssreflect.order]
lt_trans:37 [binder, in mathcomp.ssreflect.order]
lt_irr:36 [binder, in mathcomp.ssreflect.order]
lt_def:7 [binder, in mathcomp.ssreflect.order]
lt_def:2572 [binder, in mathcomp.algebra.ssrnum]
lt_def:2526 [binder, in mathcomp.algebra.ssrnum]
lt_rat_def [lemma, in mathcomp.algebra.rat]
lt_rat0 [lemma, in mathcomp.algebra.rat]
lt_ratE [lemma, in mathcomp.algebra.rat]
lt_rat [definition, in mathcomp.algebra.rat]
lt_size_deriv [lemma, in mathcomp.algebra.poly]
lt_eqmx [lemma, in mathcomp.algebra.mxalgebra]
lt0b [lemma, in mathcomp.ssreflect.ssrnat]
lt0mx [lemma, in mathcomp.algebra.mxalgebra]
lt0n [lemma, in mathcomp.ssreflect.ssrnat]
lt0n_neq0 [lemma, in mathcomp.ssreflect.ssrnat]
lt0_total:2605 [binder, in mathcomp.algebra.ssrnum]
lt0_ngt0:2600 [binder, in mathcomp.algebra.ssrnum]
lt0_mul:2598 [binder, in mathcomp.algebra.ssrnum]
lt0_add:2595 [binder, in mathcomp.algebra.ssrnum]
lt1mx [lemma, in mathcomp.algebra.mxalgebra]
lt:2570 [binder, in mathcomp.ssreflect.order]
lt:2636 [binder, in mathcomp.ssreflect.order]
lt:2670 [binder, in mathcomp.ssreflect.order]
lt:32 [binder, in mathcomp.ssreflect.order]
lt:4 [binder, in mathcomp.ssreflect.order]
lt:48 [binder, in mathcomp.ssreflect.order]
LUP_card_GL [lemma, in mathcomp.algebra.mxalgebra]
Lz:249 [binder, in mathcomp.field.galois]
L_F [abbreviation, in mathcomp.field.fieldext]
L_iso [lemma, in mathcomp.solvable.burnside_app]
L0 [abbreviation, in mathcomp.field.fieldext]
L0 [abbreviation, in mathcomp.field.fieldext]
l0 [abbreviation, in mathcomp.algebra.matrix]
l1:1688 [binder, in mathcomp.algebra.ssralg]
l2:1689 [binder, in mathcomp.algebra.ssralg]
L:1 [binder, in mathcomp.field.algC]
L:10 [binder, in mathcomp.solvable.frobenius]
L:10 [binder, in mathcomp.solvable.hall]
L:109 [binder, in mathcomp.field.finfield]
L:113 [binder, in mathcomp.solvable.frobenius]
L:114 [binder, in mathcomp.field.finfield]
L:1160 [binder, in mathcomp.ssreflect.order]
l:117 [binder, in mathcomp.solvable.commutator]
L:117 [binder, in mathcomp.field.finfield]
L:1212 [binder, in mathcomp.ssreflect.order]
L:122 [binder, in mathcomp.solvable.maximal]
L:125 [binder, in mathcomp.field.finfield]
L:126 [binder, in mathcomp.field.finfield]
L:128 [binder, in mathcomp.character.mxabelem]
L:131 [binder, in mathcomp.character.mxabelem]
l:1317 [binder, in mathcomp.algebra.matrix]
l:132 [binder, in mathcomp.ssreflect.binomial]
L:132 [binder, in mathcomp.character.mxabelem]
L:134 [binder, in mathcomp.character.mxabelem]
L:135 [binder, in mathcomp.solvable.finmodule]
L:137 [binder, in mathcomp.field.finfield]
L:140 [binder, in mathcomp.solvable.gseries]
L:143 [binder, in mathcomp.solvable.gseries]
L:147 [binder, in mathcomp.field.galois]
L:151 [binder, in mathcomp.field.galois]
l:1520 [binder, in mathcomp.ssreflect.seq]
L:159 [binder, in mathcomp.character.mxabelem]
L:160 [binder, in mathcomp.character.mxabelem]
l:1618 [binder, in mathcomp.ssreflect.seq]
L:162 [binder, in mathcomp.field.galois]
L:162 [binder, in mathcomp.character.mxabelem]
l:1627 [binder, in mathcomp.ssreflect.seq]
L:163 [binder, in mathcomp.character.mxabelem]
L:164 [binder, in mathcomp.fingroup.gproduct]
L:167 [binder, in mathcomp.character.mxabelem]
l:1682 [binder, in mathcomp.ssreflect.seq]
L:169 [binder, in mathcomp.solvable.maximal]
L:170 [binder, in mathcomp.character.mxabelem]
L:172 [binder, in mathcomp.solvable.maximal]
L:185 [binder, in mathcomp.field.galois]
L:187 [binder, in mathcomp.character.mxabelem]
L:193 [binder, in mathcomp.character.mxabelem]
L:196 [binder, in mathcomp.field.galois]
L:196 [binder, in mathcomp.character.mxabelem]
L:198 [binder, in mathcomp.character.mxabelem]
L:2072 [binder, in mathcomp.ssreflect.order]
l:2096 [binder, in mathcomp.ssreflect.order]
l:2109 [binder, in mathcomp.ssreflect.order]
L:2186 [binder, in mathcomp.ssreflect.order]
L:2190 [binder, in mathcomp.ssreflect.order]
l:2240 [binder, in mathcomp.ssreflect.order]
l:2246 [binder, in mathcomp.ssreflect.order]
L:2298 [binder, in mathcomp.ssreflect.order]
L:2300 [binder, in mathcomp.ssreflect.order]
L:2331 [binder, in mathcomp.ssreflect.order]
L:2335 [binder, in mathcomp.ssreflect.order]
L:2363 [binder, in mathcomp.ssreflect.order]
L:24 [binder, in mathcomp.character.inertia]
L:2464 [binder, in mathcomp.ssreflect.order]
L:255 [binder, in mathcomp.solvable.nilpotent]
L:256 [binder, in mathcomp.fingroup.quotient]
L:257 [binder, in mathcomp.fingroup.quotient]
L:258 [binder, in mathcomp.solvable.nilpotent]
L:2596 [binder, in mathcomp.algebra.matrix]
L:274 [binder, in mathcomp.field.fieldext]
L:274 [binder, in mathcomp.character.inertia]
L:288 [binder, in mathcomp.character.inertia]
L:290 [binder, in mathcomp.character.inertia]
L:292 [binder, in mathcomp.character.inertia]
L:295 [binder, in mathcomp.character.inertia]
L:295 [binder, in mathcomp.solvable.nilpotent]
L:32 [binder, in mathcomp.field.algebraics_fundamentals]
l:352 [binder, in mathcomp.field.closed_field]
L:360 [binder, in mathcomp.field.fieldext]
L:361 [binder, in mathcomp.field.fieldext]
L:364 [binder, in mathcomp.field.fieldext]
L:365 [binder, in mathcomp.field.fieldext]
l:393 [binder, in mathcomp.algebra.polydiv]
l:396 [binder, in mathcomp.algebra.polydiv]
l:403 [binder, in mathcomp.algebra.polydiv]
L:42 [binder, in mathcomp.character.mxabelem]
L:435 [binder, in mathcomp.algebra.intdiv]
L:436 [binder, in mathcomp.algebra.intdiv]
L:438 [binder, in mathcomp.character.inertia]
L:46 [binder, in mathcomp.character.mxabelem]
L:48 [binder, in mathcomp.character.mxabelem]
L:49 [binder, in mathcomp.character.mxabelem]
L:50 [binder, in mathcomp.field.algebraics_fundamentals]
L:50 [binder, in mathcomp.character.mxabelem]
l:507 [binder, in mathcomp.algebra.polydiv]
L:51 [binder, in mathcomp.field.algebraics_fundamentals]
l:556 [binder, in mathcomp.algebra.polydiv]
L:58 [binder, in mathcomp.field.algebraics_fundamentals]
L:59 [binder, in mathcomp.field.algebraics_fundamentals]
L:6 [binder, in mathcomp.field.algC]
L:60 [binder, in mathcomp.field.algebraics_fundamentals]
L:61 [binder, in mathcomp.field.algebraics_fundamentals]
L:65 [binder, in mathcomp.field.algebraics_fundamentals]
L:720 [binder, in mathcomp.fingroup.gproduct]
l:73 [binder, in mathcomp.field.closed_field]
L:78 [binder, in mathcomp.solvable.frobenius]
L:82 [binder, in mathcomp.solvable.frobenius]
L:85 [binder, in mathcomp.field.finfield]
L:89 [binder, in mathcomp.solvable.frobenius]
L:92 [binder, in mathcomp.solvable.frobenius]
L:96 [binder, in mathcomp.solvable.frobenius]
L:99 [binder, in mathcomp.solvable.frobenius]

---

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(565 entries)

---

Index

---

This page has been generated by coqdoc