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)

C

cancel [definition, in ssrfun]
CanChoiceMixin [definition, in choice]
CanCountMixin [definition, in choice]
CanEqMixin [definition, in eqtype]
CanFinMixin [definition, in fintype]
canF_eq [lemma, in fintype]
canF_invF [lemma, in fintype]
canF_LR [lemma, in fintype]
canF_RL [lemma, in fintype]
canF_sym [lemma, in fintype]
canLR [lemma, in ssrfun]
canRL [lemma, in ssrfun]
can2_eq [lemma, in eqtype]
can2_imset_pre [lemma, in finset]
can2_in_imset_pre [lemma, in finset]
can2_mem_pmap [lemma, in seq]
can_comp [lemma, in ssrfun]
can_eq [lemma, in eqtype]
can_imset_pre [lemma, in finset]
can_inj [lemma, in ssrfun]
can_in_inj [lemma, in ssrbool]
can_pcan [lemma, in ssrfun]
cardC [lemma, in fintype]
cardC1 [lemma, in fintype]
CardDef [moduleid, in fintype]
CardDefSig [moduleid, in fintype]
CardDefSig.card [axiom, in fintype]
CardDefSig.cardEdef [axiom, in fintype]
CardDef.card [definition, in fintype]
CardDef.cardEdef [definition, in fintype]
cardD1 [lemma, in fintype]
cardD1x [lemma, in bigops]
cardE [lemma, in fintype]
CardFunImage [section, in finset]
CardFunImage [section, in fintype]
CardFunImage.aT [variable, in finset]
CardFunImage.aT2 [variable, in finset]
CardFunImage.D [variable, in finset]
CardFunImage.D2 [variable, in finset]
CardFunImage.f [variable, in finset]
CardFunImage.f [variable, in fintype]
CardFunImage.f2 [variable, in finset]
CardFunImage.g [variable, in finset]
CardFunImage.injf [variable, in fintype]
CardFunImage.rT [variable, in finset]
CardFunImage.T [variable, in fintype]
CardFunImage.T' [variable, in fintype]
cardID [lemma, in fintype]
cardsC [lemma, in finset]
cardsCs [lemma, in finset]
cardsC1 [lemma, in finset]
cardsD1 [lemma, in finset]
cardsE [lemma, in finset]
cardsID [lemma, in finset]
CardSig [section, in fintype]
CardSig.P [variable, in fintype]
CardSig.T [variable, in fintype]
cardsT [lemma, in finset]
cardsUI [lemma, in finset]
cardsU1 [lemma, in finset]
cardsX [lemma, in finset]
cards0 [lemma, in finset]
cards0_eq [lemma, in finset]
cards1 [lemma, in finset]
cards1P [lemma, in finset]
cards2 [lemma, in finset]
cards_eq0 [lemma, in finset]
cardT [lemma, in fintype]
cardUI [lemma, in fintype]
cardU1 [lemma, in fintype]
cardX [lemma, in fintype]
card0 [lemma, in fintype]
card0_eq [lemma, in fintype]
card1 [lemma, in fintype]
card2 [lemma, in fintype]
card_bool [lemma, in fintype]
card_codom [lemma, in fintype]
card_def [abbreviation, in fintype]
card_draws [lemma, in binomial]
card_family [lemma, in finfun]
card_ffun [lemma, in finfun]
card_ffun_on [lemma, in finfun]
card_gt0 [lemma, in finset]
card_gt0P [lemma, in fintype]
card_image [lemma, in fintype]
card_imset [lemma, in finset]
card_inj_ffuns [lemma, in binomial]
card_inj_ffuns_on [lemma, in binomial]
card_in_image [lemma, in fintype]
card_in_imset [lemma, in finset]
card_ltn_sorted_tuples [lemma, in binomial]
card_option [lemma, in fintype]
card_ord [lemma, in fintype]
card_ord_partitions [lemma, in binomial]
card_partial_ord_partitions [lemma, in binomial]
card_partition [lemma, in finset]
card_pfamily [lemma, in finfun]
card_pffun_on [lemma, in finfun]
card_powerset [lemma, in finfun]
card_preim [lemma, in fintype]
card_preimset [lemma, in finset]
card_prod [lemma, in fintype]
card_sig [lemma, in fintype]
card_size [lemma, in fintype]
card_sorted_tuples [lemma, in binomial]
card_sub [lemma, in fintype]
card_sum [lemma, in fintype]
card_tagged [lemma, in fintype]
card_tuple [lemma, in tuple]
card_type [abbreviation, in fintype]
card_uniform_partition [lemma, in finset]
card_uniqP [lemma, in fintype]
card_uniq_tuples [lemma, in binomial]
card_unit [lemma, in fintype]
card_unlock [definition, in fintype]
CartesianProd [section, in finset]
CartesianProd.A1 [variable, in finset]
CartesianProd.A2 [variable, in finset]
CartesianProd.fT1 [variable, in finset]
CartesianProd.fT2 [variable, in finset]
cast_ord [definition, in fintype]
cast_ordK [lemma, in fintype]
cast_ordKV [lemma, in fintype]
cast_ord_comp [lemma, in fintype]
cast_ord_id [lemma, in fintype]
cast_ord_inj [lemma, in fintype]
cast_ord_proof [lemma, in fintype]
cat [definition, in seq]
catA [lemma, in seq]
catrev [definition, in seq]
cats0 [lemma, in seq]
cats1 [lemma, in seq]
cat0s [lemma, in seq]
cat1s [lemma, in seq]
cat_cons [lemma, in seq]
cat_monoid [definition, in bigops]
cat_nseq [lemma, in seq]
cat_rcons [lemma, in seq]
cat_take_drop [lemma, in seq]
cat_tuple [definition, in tuple]
cat_tupleP [lemma, in tuple]
cat_uniq [lemma, in seq]
Chinese [section, in div]
chinese [definition, in div]
Chinese.co_m12 [variable, in div]
Chinese.m1 [variable, in div]
Chinese.m2 [variable, in div]
chinese_modl [lemma, in div]
chinese_modlr [lemma, in div]
chinese_modr [lemma, in div]
chinese_remainder [lemma, in div]
Choice [moduleid, in choice]
choice [library]
ChoiceMixin [abbreviation, in choice]
ChoiceTheory [section, in choice]
ChoiceTheory.SubChoice [section, in choice]
ChoiceTheory.SubChoice.P [variable, in choice]
ChoiceTheory.SubChoice.sT [variable, in choice]
ChoiceTheory.T [variable, in choice]
choiceType [abbreviation, in choice]
ChoiceType [abbreviation, in choice]
Choice.base [projection, in choice]
Choice.CanMixin2 [definition, in choice]
Choice.class [definition, in choice]
Choice.Class [constructor, in choice]
Choice.class_of [record, in choice]
Choice.clone [definition, in choice]
Choice.correct [definition, in choice]
Choice.eqType [definition, in choice]
Choice.eq_nat_xchoose [lemma, in choice]
Choice.eq_pcan_xchoose [lemma, in choice]
Choice.eq_xchoose [projection, in choice]
Choice.extensional [definition, in choice]
Choice.ext0 [definition, in choice]
Choice.ext2 [projection, in choice]
Choice.Mixin [constructor, in choice]
Choice.Mixin [section, in choice]
Choice.Mixin.T [variable, in choice]
Choice.mixin_of [record, in choice]
Choice.natMixin [definition, in choice]
Choice.nat_xchooseP [lemma, in choice]
Choice.Pack [constructor, in choice]
Choice.pack [definition, in choice]
Choice.PcanMixin [section, in choice]
Choice.PcanMixin [definition, in choice]
Choice.PcanMixin.f [variable, in choice]
Choice.PcanMixin.fK [variable, in choice]
Choice.PcanMixin.f' [variable, in choice]
Choice.PcanMixin.m [variable, in choice]
Choice.PcanMixin.sT [variable, in choice]
Choice.PcanMixin.T [variable, in choice]
Choice.PcanMixin.Xfun [section, in choice]
Choice.PcanMixin.Xfun.sP [variable, in choice]
Choice.PcanMixin.Xfun.xsP [variable, in choice]
Choice.pcan_xchoose [definition, in choice]
Choice.pcan_xchooseP [lemma, in choice]
Choice.pcan_xchoose_proof [lemma, in choice]
Choice.pcan_xchoose_sig [lemma, in choice]
Choice.sort [projection, in choice]
Choice.type [record, in choice]
Choice.xchoose [projection, in choice]
Choice.xchooseP [projection, in choice]
Choice.xfun [definition, in choice]
choose [definition, in choice]
chooseP [lemma, in choice]
choose_id [lemma, in choice]
clone_pred [definition, in ssrbool]
clone_subType [definition, in eqtype]
closed [definition, in connect]
ClosedField [moduleid, in ssralg]
ClosedFieldQE [section, in closedfields]
ClosedFieldQE.axiom [variable, in closedfields]
ClosedFieldQE.F [variable, in closedfields]
closedfields [library]
ClosedFieldType [abbreviation, in ssralg]
closedFieldType [abbreviation, in ssralg]
closed_connect [lemma, in connect]
closed_fields_QEMixin [definition, in closedfields]
closure [definition, in connect]
Closure [section, in connect]
Closure.e [variable, in connect]
Closure.He [variable, in connect]
Closure.T [variable, in connect]
closure_closed [lemma, in connect]
CodeSeq [moduleid, in choice]
CodeSeq.Nat.code [definition, in choice]
CodeSeq.Nat.codeK [lemma, in choice]
CodeSeq.Nat.decode [definition, in choice]
CodeSeq.Nat.decodeK [lemma, in choice]
CodeSeq.Nat.decode_rec [definition, in choice]
CodeSeq.Seq2.code [definition, in choice]
CodeSeq.Seq2.codeK [lemma, in choice]
CodeSeq.Seq2.decode [definition, in choice]
CodeSeq.Seq2.decodeK [lemma, in choice]
CodeSeq.Seq2.pad [definition, in choice]
CodeSeq.Seq2.padding [definition, in choice]
CodeSeq.Seq2.padKl [lemma, in choice]
CodeSeq.Seq2.padKr [lemma, in choice]
CodeSeq.Seq2.Seq2 [section, in choice]
CodeSeq.Seq2.Seq2.T [variable, in choice]
CodeSeq.Seq2.strip [definition, in choice]
CodeSeq.Seq2.stripK [lemma, in choice]
codom [definition, in fintype]
codom_f [lemma, in fintype]
coefC [lemma, in poly]
coefK [lemma, in poly]
coefX [lemma, in poly]
coef0 [lemma, in poly]
coef1 [lemma, in poly]
coef_add [lemma, in poly]
coef_add_poly [lemma, in poly]
coef_Cmul [lemma, in poly]
coef_cons [lemma, in poly]
coef_deriv [lemma, in poly]
coef_derivn [lemma, in poly]
coef_map [lemma, in poly]
coef_mul [lemma, in poly]
coef_mulC [lemma, in poly]
coef_mulX [lemma, in poly]
coef_mulXn [lemma, in poly]
coef_mul_poly [lemma, in poly]
coef_mul_poly_rev [lemma, in poly]
coef_mul_rev [lemma, in poly]
coef_natmul [lemma, in poly]
coef_nderivn [lemma, in poly]
coef_negmul [lemma, in poly]
coef_opp [lemma, in poly]
coef_opp_poly [lemma, in poly]
coef_Poly [lemma, in poly]
coef_poly [lemma, in poly]
coef_sub [lemma, in poly]
coef_sum [lemma, in poly]
coef_Xmul [lemma, in poly]
coef_Xn [lemma, in poly]
coef_Xn_mul [lemma, in poly]
Combinations [section, in binomial]
commutative [definition, in ssrfun]
comm_polyX [lemma, in poly]
comm_polyXn [lemma, in poly]
comm_ringM [definition, in poly]
comp [abbreviation, in ssrfun]
comp [abbreviation, in ssrfun]
comparable [definition, in eqtype]
comparableClass [definition, in eqtype]
ComparableType [section, in eqtype]
ComparableType.Hcompare [variable, in eqtype]
ComparableType.T [variable, in eqtype]
compareb [definition, in eqtype]
CompareNatEq [constructor, in ssrnat]
CompareNatGt [constructor, in ssrnat]
CompareNatLt [constructor, in ssrnat]
compareP [lemma, in eqtype]
compare_nat [inductive, in ssrnat]
Composition [section, in ssrfun]
Composition.A [variable, in ssrfun]
Composition.B [variable, in ssrfun]
Composition.C [variable, in ssrfun]
ComRing [moduleid, in ssralg]
ComRingMixin [abbreviation, in ssralg]
ComRingType [abbreviation, in ssralg]
comRingType [abbreviation, in ssralg]
ComUnitRing [moduleid, in ssralg]
ComUnitRingMixin [abbreviation, in ssralg]
comUnitRingType [abbreviation, in ssralg]
com_coef [definition, in poly]
com_coef_poly [lemma, in poly]
com_poly [definition, in poly]
com_polyX [lemma, in poly]
com_poly0 [lemma, in poly]
com_poly1 [lemma, in poly]
congr1 [definition, in ssrfun]
congr2 [definition, in ssrfun]
congr_big [lemma, in bigops]
congr_big_nat [lemma, in bigops]
connect [definition, in connect]
Connect [section, in connect]
connect [library]
connectP [lemma, in connect]
Connect.e [variable, in connect]
Connect.T [variable, in connect]
connect0 [lemma, in connect]
connect1 [lemma, in connect]
connect_closed [lemma, in connect]
connect_root [lemma, in connect]
connect_sub [lemma, in connect]
connect_sym [definition, in connect]
connect_trans [lemma, in connect]
Cons [constructor, in seq]
cons [abbreviation, in seq]
constant [definition, in seq]
constantP [lemma, in seq]
constant_nseq [lemma, in seq]
cons_pfactor [definition, in prime]
cons_tuple [definition, in tuple]
cons_uniq [lemma, in seq]
contra [lemma, in ssrbool]
contraFF [lemma, in ssrbool]
contraFT [lemma, in ssrbool]
contraL [lemma, in ssrbool]
contraLR [lemma, in ssrbool]
contraR [lemma, in ssrbool]
contraTF [lemma, in ssrbool]
coprime [definition, in div]
coprimen1 [lemma, in div]
coprimep [definition, in polydiv]
coprimeP [lemma, in div]
coprimepP [lemma, in polydiv]
coprimepPn [lemma, in polydiv]
coprimepPW [lemma, in polydiv]
coprimep0 [lemma, in polydiv]
coprimep1 [lemma, in polydiv]
coprimep_dvdl [lemma, in polydiv]
coprimep_sym [lemma, in polydiv]
coprime0p [lemma, in polydiv]
coprime1n [lemma, in div]
coprime1p [lemma, in polydiv]
coprime_dvdl [lemma, in div]
coprime_dvdr [lemma, in div]
coprime_egcdn [lemma, in div]
coprime_expl [lemma, in div]
coprime_expr [lemma, in div]
coprime_has_primes [lemma, in prime]
coprime_modl [lemma, in div]
coprime_modr [lemma, in div]
coprime_mull [lemma, in div]
coprime_mulr [lemma, in div]
coprime_partC [lemma, in prime]
coprime_pexpl [lemma, in div]
coprime_pexpr [lemma, in div]
coprime_pi' [lemma, in prime]
coprime_sym [lemma, in div]
count [definition, in seq]
Countable [moduleid, in choice]
CountableTheory [section, in choice]
CountableTheory.T [variable, in choice]
Countable.base [projection, in choice]
Countable.ChoiceMixin [definition, in choice]
Countable.choiceType [definition, in choice]
Countable.Class [constructor, in choice]
Countable.class [definition, in choice]
Countable.class_of [record, in choice]
Countable.clone [definition, in choice]
Countable.EqMixin [definition, in choice]
Countable.eqType [definition, in choice]
Countable.ext [projection, in choice]
Countable.Mixin [constructor, in choice]
Countable.mixin_of [record, in choice]
Countable.pack [definition, in choice]
Countable.Pack [constructor, in choice]
Countable.pickle [projection, in choice]
Countable.pickleK [projection, in choice]
Countable.PickleSeq [section, in choice]
Countable.PickleSeq.p [variable, in choice]
Countable.PickleSeq.pK [variable, in choice]
Countable.PickleSeq.T [variable, in choice]
Countable.PickleSeq.u [variable, in choice]
Countable.pickle_seq [definition, in choice]
Countable.pickle_seqK [lemma, in choice]
Countable.sort [projection, in choice]
Countable.type [record, in choice]
Countable.unpickle [projection, in choice]
Countable.unpickle_seq [definition, in choice]
CountChoiceMixin [abbreviation, in choice]
CountMixin [abbreviation, in choice]
countType [abbreviation, in choice]
CountType [abbreviation, in choice]
count_cat [lemma, in seq]
count_filter [lemma, in seq]
count_map [lemma, in seq]
count_mem_uniq [lemma, in seq]
count_predC [lemma, in seq]
count_predT [lemma, in seq]
count_predUI [lemma, in seq]
count_pred0 [lemma, in seq]
count_size [lemma, in seq]
count_uniq_mem [lemma, in seq]
cover [definition, in finset]
cover_at [definition, in finset]
cover_at_eq [lemma, in finset]
cover_at_mem [lemma, in finset]
cover_setI [lemma, in finset]
curry_imset2l [lemma, in finset]
curry_imset2r [lemma, in finset]
curry_imset2X [lemma, in finset]
cycle [definition, in paths]
CycleArc [section, in paths]
CycleArc.T [variable, in paths]
cycle_from_next [lemma, in paths]
cycle_from_prev [lemma, in paths]
cycle_next [lemma, in paths]
cycle_orbit [lemma, in connect]
cycle_path [lemma, in paths]
cycle_prev [lemma, in paths]
cycle_rot [lemma, in paths]
cycle_rotr [lemma, in paths]

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)