Top

B (Definitions)

Files

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

_

Definitions

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

_

Lemmas

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

_

Abbreviations

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

_

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

_

Notations

B (Definitions)

baseAspace [def, in mathcomp.field.fieldext]
baseField_scale [def, in mathcomp.field.fieldext]
baseFieldType [def, in mathcomp.field.fieldext]
BaseGroup.pack_ [def, in mathcomp.boot.monoid]
BaseGroup.phant_clone [def, in mathcomp.boot.monoid]
BaseGroup.phant_on_ [def, in mathcomp.boot.monoid]
BaseUMagma.pack_ [def, in mathcomp.boot.monoid]
BaseUMagma.phant_clone [def, in mathcomp.boot.monoid]
BaseUMagma.phant_on_ [def, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.identity_builder [def, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.phant_axioms [def, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.phant_Build [def, in mathcomp.boot.monoid]
baseVspace [def, in mathcomp.field.fieldext]
basis_of [def, in mathcomp.algebra.vector]
behead [def, in mathcomp.boot.seq]
behead_bseq [def, in mathcomp.boot.tuple]
behead_tuple [def, in mathcomp.boot.tuple]
belast [def, in mathcomp.boot.seq]
belast_bseq [def, in mathcomp.boot.tuple]
belast_tuple [def, in mathcomp.boot.tuple]
Bezout_rec [def, in mathcomp.boot.div]
bgFunc_id [def, in mathcomp.solvable.gfunctor]
bigcap_group [def, in mathcomp.finite_group.fingroup]
bigop.body [def, in mathcomp.boot.bigop]
bigop.unlock [def, in mathcomp.boot.bigop]
bigop_unlock [def, in mathcomp.boot.bigop]
bigop_unlock_subterm [def, in mathcomp.boot.bigop]
Bilinear.pack_ [def, in mathcomp.algebra.sesquilinear]
Bilinear.phant_clone [def, in mathcomp.algebra.sesquilinear]
Bilinear.phant_on_ [def, in mathcomp.algebra.sesquilinear]
bilinear_for [def, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear.phant_axioms [def, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear.phant_Build [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.map_at_both [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.map_at_left [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.map_at_right [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.map_class [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.unify_map_at_both [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.unify_map_at_left [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.unify_map_at_right [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.wrap [def, in mathcomp.algebra.sesquilinear]
bin_of_nat [def, in mathcomp.boot.ssrnat]
binary_addv_expr [def, in mathcomp.algebra.vector]
binary_mxsum_expr [def, in mathcomp.algebra.mxalgebra]
binomial [def, in mathcomp.boot.binomial]
bitseq [def, in mathcomp.boot.seq]
bitseq_predType [def, in mathcomp.boot.seq]
block_mx [def, in mathcomp.algebra.matrix]
block_mxAx [def, in mathcomp.algebra.matrix]
bnd_simp [def, in mathcomp.algebra.interval]
bound_in_itv [def, in mathcomp.algebra.interval]
bound_join [def, in mathcomp.algebra.interval]
bound_meet [def, in mathcomp.algebra.interval]
bseq [def, in mathcomp.boot.tuple]
bseq_hasChoice [def, in mathcomp.boot.tuple]
bseq_hasDecEq [def, in mathcomp.boot.tuple]
bseq_isCountable [def, in mathcomp.boot.tuple]
bseq_of_tuple [def, in mathcomp.boot.tuple]
bseq_predType [def, in mathcomp.boot.tuple]
bseq_tagged_tuple [def, in mathcomp.boot.tuple]
Builders_1.i [def, in mathcomp.field.algC]
Builders_1.le [def, in mathcomp.field.algC]
Builders_1.lt [def, in mathcomp.field.algC]
Builders_1.norm [def, in mathcomp.field.algC]
Builders_1.sqrt [def, in mathcomp.field.algC]
Builders_1.v2r [def, in mathcomp.algebra.vector]
Builders_26.sub_enum [def, in mathcomp.boot.fintype]
Builders_26.SubFinMixin [def, in mathcomp.boot.fintype]
bump [def, in mathcomp.boot.fintype]