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)

P

pack_subCountType [definition, in choice]
pack_subFinType [definition, in fintype]
pairmap [definition, in seq]
pairmapK [lemma, in seq]
pairmap_tuple [definition, in tuple]
pairmap_tupleP [lemma, in tuple]
pair_big [lemma, in bigops]
pair_bigA [lemma, in bigops]
pair_big_dep [lemma, in bigops]
pair_eq [definition, in eqtype]
pair_eqE [lemma, in eqtype]
pair_eqP [lemma, in eqtype]
pair_eq1 [lemma, in eqtype]
pair_eq2 [lemma, in eqtype]
pair_of_tag [definition, in choice]
pair_of_tagK [lemma, in choice]
partition [definition, in finset]
Partitions [section, in finset]
Partitions.BigOps [section, in finset]
Partitions.BigOps.idx [variable, in finset]
Partitions.BigOps.op [variable, in finset]
Partitions.BigOps.R [variable, in finset]
Partitions.Preim [section, in finset]
Partitions.Preim.f [variable, in finset]
Partitions.Preim.rT [variable, in finset]
Partitions.T [variable, in finset]
partition_big [lemma, in bigops]
partition_big_imset [lemma, in finset]
partn [definition, in prime]
partnC [lemma, in prime]
partnI [lemma, in prime]
partnNK [lemma, in prime]
partnT [lemma, in prime]
partn0 [lemma, in prime]
partn1 [lemma, in prime]
partn_biggcd [lemma, in prime]
partn_biglcm [lemma, in prime]
partn_dvd [lemma, in prime]
partn_eq1 [lemma, in prime]
partn_exp [lemma, in prime]
partn_gcd [lemma, in prime]
partn_lcm [lemma, in prime]
partn_mul [lemma, in prime]
partn_part [lemma, in prime]
partn_pi [lemma, in prime]
part_gt0 [lemma, in prime]
part_pnat [lemma, in prime]
part_pnat_id [lemma, in prime]
part_p'nat [lemma, in prime]
Pascal [lemma, in binomial]
path [definition, in paths]
pathP [lemma, in paths]
Paths [section, in paths]
paths [library]
Paths.n0 [variable, in paths]
Paths.Path [section, in paths]
Paths.Path.e [variable, in paths]
Paths.Path.x0_cycle [variable, in paths]
Paths.T [variable, in paths]
path_cat [lemma, in paths]
path_connect [lemma, in connect]
path_map [lemma, in paths]
path_merge [lemma, in paths]
path_min_sorted [lemma, in paths]
path_rcons [lemma, in paths]
path_rev [lemma, in paths]
path_sorted [lemma, in paths]
pcancel [definition, in ssrfun]
PcanChoiceMixin [definition, in choice]
PcanCountMixin [definition, in choice]
PcanEqMixin [definition, in eqtype]
PcanFinMixin [definition, in fintype]
pcan_enumP [lemma, in fintype]
pcan_inj [lemma, in ssrfun]
pcan_pcomp [lemma, in ssrfun]
pcan_pickleK [lemma, in choice]
pcomp [definition, in ssrfun]
pdiv [definition, in prime]
pdivP [lemma, in prime]
pdiv_dvd [lemma, in prime]
pdiv_gt0 [lemma, in prime]
pdiv_id [lemma, in prime]
pdiv_leq [lemma, in prime]
pdiv_min_dvd [lemma, in prime]
pdiv_pfactor [lemma, in prime]
pdiv_prime [lemma, in prime]
PermSeq [section, in seq]
PermSeq.T [variable, in seq]
perm_catAC [lemma, in seq]
perm_catC [lemma, in seq]
perm_catCA [lemma, in seq]
perm_cat2l [lemma, in seq]
perm_cat2r [lemma, in seq]
perm_cons [lemma, in seq]
perm_eq [definition, in seq]
perm_eql [abbreviation, in seq]
perm_eql [abbreviation, in seq]
perm_eqlP [lemma, in seq]
perm_eqP [lemma, in seq]
perm_eqr [abbreviation, in seq]
perm_eqr [abbreviation, in seq]
perm_eqrP [lemma, in seq]
perm_eq_mem [lemma, in seq]
perm_eq_refl [lemma, in seq]
perm_eq_size [lemma, in seq]
perm_eq_sym [lemma, in seq]
perm_eq_trans [lemma, in seq]
perm_eq_uniq [lemma, in seq]
perm_merge [lemma, in paths]
perm_rcons [lemma, in seq]
perm_rot [lemma, in seq]
perm_rotr [lemma, in seq]
perm_sort [lemma, in paths]
perm_sortP [lemma, in paths]
perm_uniq [lemma, in seq]
PervasiveMonoids [section, in bigops]
pfactor [definition, in prime]
pfactorK [lemma, in prime]
pfactor_coprime [lemma, in prime]
pfactor_dvdn [lemma, in prime]
pfactor_dvdnn [lemma, in prime]
pfactor_gt0 [lemma, in prime]
pfamily [definition, in finfun]
pfamilyP [lemma, in finfun]
pffun_on [definition, in finfun]
pffun_onP [lemma, in finfun]
pfRM [definition, in poly]
ph [abbreviation, in ssrbool]
ph [abbreviation, in ssrbool]
Phant [constructor, in ssreflect]
phant [inductive, in ssreflect]
Phantom [constructor, in ssreflect]
phantom [inductive, in ssreflect]
phant_id [definition, in ssrfun]
phi [definition, in prime]
phiE [lemma, in prime]
phi_coprime [lemma, in prime]
phi_count_coprime [lemma, in prime]
phi_gt0 [lemma, in prime]
phi_pfactor [lemma, in prime]
Pick [constructor, in fintype]
pick [definition, in fintype]
pickle [definition, in choice]
pickleK [lemma, in choice]
pickleK_inv [lemma, in choice]
pickle_inv [definition, in choice]
pickle_invK [lemma, in choice]
pickP [lemma, in fintype]
pick_spec [inductive, in fintype]
PiNat [section, in prime]
pi_max_pdiv [lemma, in prime]
pi_of [definition, in prime]
pi_of_exp [lemma, in prime]
pi_of_prime [lemma, in prime]
pi_pdiv [lemma, in prime]
pi_pnat [lemma, in prime]
PlainTheory [section, in finfun]
PlainTheory.aT [variable, in finfun]
PlainTheory.Family [section, in finfun]
PlainTheory.Family.F [variable, in finfun]
PlainTheory.rT [variable, in finfun]
plusE [lemma, in ssrnat]
Pmap [section, in seq]
pmap [definition, in seq]
pmapS_filter [lemma, in seq]
Pmapub [section, in seq]
Pmapub.p [variable, in seq]
Pmapub.sT [variable, in seq]
Pmapub.T [variable, in seq]
Pmap.aT [variable, in seq]
Pmap.f [variable, in seq]
Pmap.fK [variable, in seq]
Pmap.g [variable, in seq]
Pmap.rT [variable, in seq]
pmap_filter [lemma, in seq]
pmap_sub_uniq [lemma, in seq]
pmap_uniq [lemma, in seq]
pnat [definition, in prime]
pnatE [lemma, in prime]
pnatI [lemma, in prime]
pnatNK [lemma, in prime]
pnatP [lemma, in prime]
pnat_coprime [lemma, in prime]
pnat_div [lemma, in prime]
pnat_dvd [lemma, in prime]
pnat_exp [lemma, in prime]
pnat_id [lemma, in prime]
pnat_mul [lemma, in prime]
pnat_pi [lemma, in prime]
pnat_1 [lemma, in prime]
Poly [definition, in poly]
poly [library]
polyC [definition, in poly]
polyC0 [lemma, in poly]
polyC1 [lemma, in poly]
polyC_add [lemma, in poly]
polyC_eq0 [lemma, in poly]
polyC_exp [lemma, in poly]
polyC_inj [lemma, in poly]
polyC_mul [lemma, in poly]
polyC_natmul [lemma, in poly]
polyC_opp [lemma, in poly]
polyC_RM [lemma, in poly]
polyC_sub [lemma, in poly]
polydiv [library]
polyF [definition, in closedfields]
PolyK [lemma, in poly]
Polynomial [constructor, in poly]
polynomial [record, in poly]
Polynomial [section, in poly]
PolynomialComRing [section, in poly]
PolynomialComRing.R [variable, in poly]
PolynomialIdomain [section, in poly]
PolynomialIdomain.R [variable, in poly]
PolynomialTheory [section, in poly]
PolynomialTheory.R [variable, in poly]
Polynomial.R [variable, in poly]
polynomial_choiceMixin [definition, in poly]
polynomial_choiceType [definition, in poly]
polynomial_comRingType [definition, in poly]
polynomial_comUnitRingType [definition, in poly]
polynomial_eqMixin [definition, in poly]
polynomial_eqType [definition, in poly]
polynomial_idomainType [definition, in poly]
polynomial_lmodType [definition, in poly]
polynomial_ncalgebraType [definition, in poly]
polynomial_ringType [definition, in poly]
polynomial_subType [definition, in poly]
polynomial_unitRingType [definition, in poly]
polynomial_zmodType [definition, in poly]
polyP [lemma, in poly]
polyseq [projection, in poly]
polyseqC [lemma, in poly]
polyseqK [lemma, in poly]
polyseqX [lemma, in poly]
polyseq1 [lemma, in poly]
polyseq_cons [lemma, in poly]
polyseq_poly [lemma, in poly]
polySpred [lemma, in poly]
polyX [definition, in poly]
poly0Vpos [lemma, in poly]
poly_choiceType [definition, in poly]
poly_comRingType [definition, in poly]
poly_comUnitRingType [definition, in poly]
poly_cons [definition, in poly]
poly_cons_def [lemma, in poly]
poly_def [lemma, in poly]
poly_eqType [definition, in poly]
poly_idomainMixin [lemma, in poly]
poly_idomainType [definition, in poly]
poly_ind [lemma, in poly]
poly_initial [lemma, in poly]
poly_inj [lemma, in poly]
poly_intro_unit [lemma, in poly]
poly_inv [definition, in poly]
poly_inv_out [lemma, in poly]
poly_lmodMixin [definition, in poly]
poly_lmodType [definition, in poly]
poly_morphRM [definition, in poly]
poly_morphX_comm [lemma, in poly]
poly_mulC [lemma, in poly]
poly_mulVp [lemma, in poly]
poly_ncalgebraType [definition, in poly]
poly_of [definition, in poly]
poly_ringMixin [definition, in poly]
poly_ringType [definition, in poly]
poly_subType [definition, in poly]
poly_unit [definition, in poly]
poly_unitRingMixin [definition, in poly]
poly_unitRingType [definition, in poly]
poly_zmodMixin [definition, in poly]
poly_zmodType [definition, in poly]
pop_succn [definition, in ssrnat]
PosNotEq0 [constructor, in ssrnat]
posnP [lemma, in ssrnat]
pos_of_nat [definition, in ssrnat]
powerset [definition, in finfun]
pred [definition, in ssrbool]
predArgType [definition, in ssrbool]
predC [definition, in ssrbool]
predC1 [definition, in eqtype]
predC_closed [lemma, in connect]
predD [definition, in ssrbool]
predD1 [definition, in eqtype]
predD1P [lemma, in eqtype]
predE [lemma, in ssrnat]
predI [definition, in ssrbool]
Predicates [section, in ssrbool]
Predicates.T [variable, in ssrbool]
predn [definition, in ssrnat]
prednK [lemma, in ssrnat]
predn_exp [lemma, in binomial]
predn_sub [lemma, in ssrnat]
predn_subS [lemma, in ssrnat]
predPredType [definition, in ssrbool]
predT [definition, in ssrbool]
PredType [constructor, in ssrbool]
predType [record, in ssrbool]
predT_subset [lemma, in fintype]
predU [definition, in ssrbool]
predU1 [definition, in eqtype]
predU1l [lemma, in eqtype]
predU1P [lemma, in eqtype]
predU1r [lemma, in eqtype]
predX [definition, in eqtype]
predX_prod_enum [lemma, in fintype]
pred0 [definition, in ssrbool]
pred0b [definition, in fintype]
pred0P [lemma, in fintype]
pred0Pn [lemma, in fintype]
pred1 [definition, in eqtype]
pred1E [lemma, in eqtype]
pred2 [definition, in eqtype]
pred2P [lemma, in eqtype]
pred3 [definition, in eqtype]
pred4 [definition, in eqtype]
pred_class [abbreviation, in ssrbool]
pred_of_argType [definition, in ssrbool]
pred_of_eq_seq [definition, in seq]
pred_of_mem [definition, in ssrbool]
pred_of_mem_pred [definition, in ssrbool]
pred_of_set [abbreviation, in finset]
pred_of_set_def [abbreviation, in finset]
pred_of_set_unlock [definition, in finset]
pred_of_simpl [definition, in ssrbool]
pred_sort [projection, in ssrbool]
preim [definition, in ssrbool]
preimset [definition, in finset]
preimsetC [lemma, in finset]
preimsetD [lemma, in finset]
preimsetI [lemma, in finset]
preimsetS [lemma, in finset]
preimsetT [lemma, in finset]
preimsetU [lemma, in finset]
preimset0 [lemma, in finset]
preimset_proper [lemma, in finset]
preim_at [definition, in finset]
preim_iinv [lemma, in fintype]
preim_partition [definition, in finset]
preim_partitionP [lemma, in finset]
preim_seq [definition, in fintype]
prev [definition, in paths]
prev_at [definition, in paths]
prev_cycle [lemma, in paths]
prev_map [lemma, in paths]
prev_next [lemma, in paths]
prev_nth [lemma, in paths]
prev_rev [lemma, in paths]
prev_rot [lemma, in paths]
prev_rotr [lemma, in paths]
pre_image [lemma, in fintype]
pre_symmetric [definition, in ssrbool]
prime [definition, in prime]
prime [library]
primeP [lemma, in prime]
primePn [lemma, in prime]
primePns [lemma, in prime]
primes [definition, in prime]
primes_exp [lemma, in prime]
primes_mul [lemma, in prime]
primes_part [lemma, in prime]
primes_prime [lemma, in prime]
primes_uniq [lemma, in prime]
prime_coprime [lemma, in prime]
prime_decomp [section, in prime]
prime_decomp [definition, in prime]
prime_decompE [lemma, in prime]
prime_decomp_correct [lemma, in prime]
prime_decomp_rec [definition, in prime]
prime_dvd_bin [lemma, in binomial]
prime_gt0 [lemma, in prime]
prime_gt1 [lemma, in prime]
ProdEqType [section, in eqtype]
ProdEqType.T1 [variable, in eqtype]
ProdEqType.T2 [variable, in eqtype]
ProdFinType [section, in fintype]
ProdFinType.T1 [variable, in fintype]
ProdFinType.T2 [variable, in fintype]
prodn_cond_gt0 [lemma, in bigops]
prodn_gt0 [lemma, in bigops]
prod_choiceMixin [definition, in choice]
prod_choiceType [definition, in choice]
prod_countMixin [definition, in choice]
prod_countType [definition, in choice]
prod_enum [definition, in fintype]
prod_enumP [lemma, in fintype]
prod_eqMixin [definition, in eqtype]
prod_eqType [definition, in eqtype]
prod_finMixin [definition, in fintype]
prod_finType [definition, in fintype]
prod_nat_const [lemma, in bigops]
prod_nat_const_nat [lemma, in bigops]
prod_prime_decomp [lemma, in prime]
proper [definition, in fintype]
properD [lemma, in finset]
properD1 [lemma, in finset]
properE [lemma, in fintype]
properEcard [lemma, in finset]
properEneq [lemma, in finset]
properI [lemma, in finset]
properIl [lemma, in finset]
properIr [lemma, in finset]
properIset [lemma, in finset]
properP [lemma, in fintype]
properT [lemma, in finset]
properU [lemma, in finset]
properUl [lemma, in finset]
properUr [lemma, in finset]
proper0 [lemma, in finset]
proper1set [lemma, in finset]
proper_card [lemma, in fintype]
proper_irrefl [lemma, in fintype]
proper_neq [lemma, in finset]
proper_sub [lemma, in fintype]
proper_subn [lemma, in fintype]
proper_sub_trans [lemma, in fintype]
proper_trans [lemma, in fintype]
prop_congr [lemma, in ssrbool]
prop_for [definition, in ssrbool]
prop_in1 [definition, in ssrbool]
prop_in11 [definition, in ssrbool]
prop_in111 [definition, in ssrbool]
prop_in12 [definition, in ssrbool]
prop_in2 [definition, in ssrbool]
prop_in21 [definition, in ssrbool]
prop_in3 [definition, in ssrbool]
prop_on1 [definition, in ssrbool]
prop_on2 [definition, in ssrbool]
protect_term [definition, in ssreflect]
p'natE [lemma, in prime]
p_natP [lemma, in prime]
p_part [lemma, in prime]
p_part_eq1 [lemma, in prime]
p_part_gt1 [lemma, in prime]

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)