closedfields

Global Index

J

K

Y

_

(5434 entries)

Projection Index

A

D

H

I

J

K

L

N

O

Q

W

X

Y

Z

_

(89 entries)

Record Index

A

B

D

H

I

J

K

L

O

Q

V

X

Y

Z

_

(58 entries)

Lemma Index

J

K

Q

Y

_

(2752 entries)

Section Index

H

J

K

V

W

X

Y

_

(233 entries)

Constructor Index

H

J

K

Q

V

X

Y

Z

_

(145 entries)

Abbreviation Index

H

J

K

M

V

W

Y

_

(139 entries)

Inductive Index

H

J

K

N

Q

V

W

X

Y

Z

_

(50 entries)

Definition Index

J

K

Q

V

Y

_

(1267 entries)

Moduleid Index

B

H

J

K

P

V

W

X

Y

_

(47 entries)

Axiom Index

A

B

D

G

H

J

K

L

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

(24 entries)

Variable Index

H

J

K

V

W

X

Y

_

(609 entries)

Library Index

A

G

H

I

J

K

L

M

N

O

Q

R

U

V

W

X

Y

Z

_

(21 entries)

R

rabstrX [lemma, in closedfields]
ramulXnT [lemma, in closedfields]
rcons [definition, in seq]
rcons_cat [lemma, in seq]
rcons_cons [lemma, in seq]
rcons_uniq [lemma, in seq]
ReduceBig [moduleid, in bigops]
reducebig [definition, in bigops]
ReduceBigSig [moduleid, in bigops]
ReduceBigSig.bigop [axiom, in bigops]
ReduceBigSig.bigopE [axiom, in bigops]
ReduceBig.bigop [definition, in bigops]
ReduceBig.bigopE [lemma, in bigops]
reduce_big_unlock [definition, in bigops]
reflect [inductive, in ssrbool]
Reflect [section, in ssrbool]
ReflectConnectives [section, in ssrbool]
ReflectConnectives.b1 [variable, in ssrbool]
ReflectConnectives.b2 [variable, in ssrbool]
ReflectConnectives.b3 [variable, in ssrbool]
ReflectConnectives.b4 [variable, in ssrbool]
ReflectConnectives.b5 [variable, in ssrbool]
ReflectCore [section, in ssrbool]
ReflectCore.b [variable, in ssrbool]
ReflectCore.c [variable, in ssrbool]
ReflectCore.Hb [variable, in ssrbool]
ReflectCore.P [variable, in ssrbool]
ReflectCore.Q [variable, in ssrbool]
ReflectF [constructor, in ssrbool]
ReflectNegCore [section, in ssrbool]
ReflectNegCore.b [variable, in ssrbool]
ReflectNegCore.c [variable, in ssrbool]
ReflectNegCore.Hb [variable, in ssrbool]
ReflectNegCore.P [variable, in ssrbool]
ReflectNegCore.Q [variable, in ssrbool]
ReflectT [constructor, in ssrbool]
Reflect.b [variable, in ssrbool]
Reflect.b' [variable, in ssrbool]
Reflect.c [variable, in ssrbool]
Reflect.P [variable, in ssrbool]
Reflect.Pb [variable, in ssrbool]
Reflect.Pb' [variable, in ssrbool]
Reflect.Q [variable, in ssrbool]
reflexive [definition, in ssrbool]
reindex [lemma, in bigops]
reindex_inj [lemma, in bigops]
reindex_onto [lemma, in bigops]
rel [definition, in ssrbool]
RelAdjunction [section, in connect]
RelAdjunction [constructor, in connect]
RelAdjunction.a [variable, in connect]
RelAdjunction.e [variable, in connect]
RelAdjunction.e' [variable, in connect]
RelAdjunction.h [variable, in connect]
RelAdjunction.Ha [variable, in connect]
RelAdjunction.He [variable, in connect]
RelAdjunction.He' [variable, in connect]
RelAdjunction.T [variable, in connect]
RelAdjunction.T' [variable, in connect]
RelationProperties [section, in ssrbool]
RelationProperties.R [variable, in ssrbool]
RelationProperties.T [variable, in ssrbool]
relU [definition, in ssrbool]
relU_sym [lemma, in connect]
rel_adjunction [record, in connect]
rel_base [definition, in paths]
rel_functor [projection, in connect]
rel_of_simpl_rel [definition, in ssrbool]
rel_unit [projection, in connect]
reshape [definition, in seq]
reshapeKl [lemma, in seq]
reshapeKr [lemma, in seq]
returnType [definition, in ssreflect]
rev [definition, in seq]
Rev [section, in seq]
revK [lemma, in seq]
RevRingType [abbreviation, in ssralg]
Rev.T [variable, in seq]
rev_cat [lemma, in seq]
rev_cons [lemma, in seq]
rev_left_loop [definition, in ssrfun]
rev_ord [definition, in fintype]
rev_ordK [lemma, in fintype]
rev_ord_inj [lemma, in fintype]
rev_ord_proof [lemma, in fintype]
rev_rcons [lemma, in seq]
rev_right_loop [definition, in ssrfun]
rev_rot [lemma, in seq]
rev_rotr [lemma, in seq]
rev_trans [lemma, in ssrbool]
rev_tuple [definition, in tuple]
rev_tupleP [lemma, in tuple]
rev_uniq [lemma, in seq]
rhs [definition, in finset]
right_arc [lemma, in paths]
right_commutative [definition, in ssrfun]
right_distributive [definition, in ssrfun]
right_id [definition, in ssrfun]
right_injective [definition, in ssrfun]
right_inverse [definition, in ssrfun]
right_loop [definition, in ssrfun]
right_transitive [definition, in ssrbool]
right_zero [definition, in ssrfun]
Ring [moduleid, in ssralg]
RingMixin [abbreviation, in ssralg]
ringType [abbreviation, in ssralg]
RingType [abbreviation, in ssralg]
rmulpT [lemma, in closedfields]
root [definition, in connect]
root [definition, in poly]
rootP [lemma, in connect]
roots [definition, in connect]
roots_root [lemma, in connect]
root0 [lemma, in polydiv]
root1n [lemma, in polydiv]
root_biggcd [lemma, in polydiv]
root_bigmul [lemma, in polydiv]
root_connect [lemma, in connect]
root_factor_theorem [lemma, in poly]
root_field_map_poly [lemma, in poly]
root_gcd [lemma, in polydiv]
root_gdco [lemma, in polydiv]
root_map_poly [lemma, in poly]
root_mul [lemma, in polydiv]
root_root [lemma, in connect]
root_size_neq1 [lemma, in polydiv]
rot [definition, in seq]
RotCompLemmas [section, in seq]
RotCompLemmas.T [variable, in seq]
rotK [lemma, in seq]
rotr [definition, in seq]
rotrK [lemma, in seq]
RotrLemmas [section, in seq]
RotrLemmas.n0 [variable, in seq]
RotrLemmas.T [variable, in seq]
RotrLemmas.T' [variable, in seq]
rotr1_rcons [lemma, in seq]
rotr_inj [lemma, in seq]
rotr_rotr [lemma, in seq]
rotr_size_cat [lemma, in seq]
rotr_tuple [definition, in tuple]
rotr_tupleP [lemma, in tuple]
rotr_uniq [lemma, in seq]
rotS [lemma, in seq]
RotToArcSpec [constructor, in paths]
RotToSpec [constructor, in seq]
rot0 [lemma, in seq]
rot1_cons [lemma, in seq]
rot_addn [lemma, in seq]
rot_add_mod [lemma, in seq]
rot_inj [lemma, in seq]
rot_oversize [lemma, in seq]
rot_rot [lemma, in seq]
rot_rotr [lemma, in seq]
rot_size [lemma, in seq]
rot_size_cat [lemma, in seq]
rot_to [lemma, in seq]
rot_to_arc [lemma, in paths]
rot_to_arc_spec [inductive, in paths]
rot_to_spec [inductive, in seq]
rot_tuple [definition, in tuple]
rot_tupleP [lemma, in tuple]
rot_uniq [lemma, in seq]
rpoly [definition, in closedfields]
rpoly_map_mul [lemma, in closedfields]
rrefl [lemma, in ssrfun]
rseq_poly [definition, in closedfields]
rseq_poly_map [lemma, in closedfields]
rshift [definition, in fintype]
rshift_subproof [lemma, in fintype]
rsumpT [lemma, in closedfields]

Global Index

J

K

Y

_

(5434 entries)

Projection Index

A

D

H

I

J

K

L

N

O

Q

W

X

Y

Z

_

(89 entries)

Record Index

A

B

D

H

I

J

K

L

O

Q

V

X

Y

Z

_

(58 entries)

Lemma Index

J

K

Q

Y

_

(2752 entries)

Section Index

H

J

K

V

W

X

Y

_

(233 entries)

Constructor Index

H

J

K

Q

V

X

Y

Z

_

(145 entries)

Abbreviation Index

H

J

K

M

V

W

Y

_

(139 entries)

Inductive Index

H

J

K

N

Q

V

W

X

Y

Z

_

(50 entries)

Definition Index

J

K

Q

V

Y

_

(1267 entries)

Moduleid Index

B

H

J

K

P

V

W

X

Y

_

(47 entries)

Axiom Index

A

B

D

G

H

J

K

L

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

(24 entries)

Variable Index

H

J

K

V

W

X

Y

_

(609 entries)

Library Index

A

G

H

I

J

K

L

M

N

O

Q

R

U

V

W

X

Y

Z

_

(21 entries)