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)

E

edivn [definition, in div]
edivnP [lemma, in div]
EdivnSpec [constructor, in div]
edivn2 [definition, in prime]
edivn2P [lemma, in prime]
edivn_def [lemma, in div]
edivn_eq [lemma, in div]
edivn_rec [definition, in div]
edivn_spec [inductive, in div]
edivp [definition, in poly]
edivpT [definition, in closedfields]
edivpTP [lemma, in closedfields]
edivpT_qf [lemma, in closedfields]
edivp_map [lemma, in poly]
edivp_mod_spec [lemma, in poly]
edivp_mon_spec [lemma, in poly]
edivp_rec [definition, in poly]
edivp_rec_loop [definition, in closedfields]
edivp_rec_loopP [lemma, in closedfields]
edivp_rec_loopT [definition, in closedfields]
edivp_rec_loopTP [lemma, in closedfields]
edivp_rec_loopT_qf [lemma, in closedfields]
edivp_scal_spec [lemma, in poly]
edivp_spec [lemma, in poly]
egcdn [definition, in div]
egcdnP [lemma, in div]
EgcdnSpec [constructor, in div]
egcdn_rec [definition, in div]
egcdn_spec [inductive, in div]
egcdp [definition, in polydiv]
egcdpPS [lemma, in polydiv]
egcdpPW [lemma, in polydiv]
egcdp_rec [definition, in polydiv]
egcdp_recP [lemma, in polydiv]
egcd0n [lemma, in div]
elimF [lemma, in ssrbool]
elimFn [lemma, in ssrbool]
elimN [lemma, in ssrbool]
elimNf [lemma, in ssrbool]
elimNTF [lemma, in ssrbool]
elimT [lemma, in ssrbool]
elimTF [lemma, in ssrbool]
elimTFn [lemma, in ssrbool]
elimTn [lemma, in ssrbool]
elogn2 [definition, in prime]
elogn2P [lemma, in prime]
Elogn2Spec [constructor, in prime]
elogn2_spec [inductive, in prime]
enum [definition, in fintype]
EnumDef [moduleid, in fintype]
enumP [lemma, in fintype]
EnumRank [section, in fintype]
EnumRank.T [variable, in fintype]
EnumSig [moduleid, in fintype]
enumT [lemma, in fintype]
enum0 [lemma, in fintype]
enum1 [lemma, in fintype]
enum_default [lemma, in fintype]
enum_ordS [lemma, in fintype]
enum_rank [definition, in fintype]
enum_rankK [lemma, in fintype]
enum_rank_bij [lemma, in fintype]
enum_rank_inj [lemma, in fintype]
enum_rank_ord [lemma, in fintype]
enum_rank_subproof [lemma, in fintype]
enum_tuple [definition, in tuple]
enum_tupleP [lemma, in tuple]
enum_uniq [lemma, in fintype]
enum_val [definition, in fintype]
enum_valK [lemma, in fintype]
enum_val_bij [lemma, in fintype]
enum_val_inj [lemma, in fintype]
enum_val_nth [lemma, in fintype]
enum_val_ord [lemma, in fintype]
eqbE [lemma, in eqtype]
eqbP [lemma, in eqtype]
EqConnect [section, in connect]
EqConnect.T [variable, in connect]
eqE [lemma, in eqtype]
eqEcard [lemma, in finset]
eqEproper [lemma, in finset]
eqEsubset [lemma, in finset]
EqFun [section, in eqtype]
eqfun [definition, in ssrfun]
EqFun.aT [variable, in eqtype]
EqFun.Endo [section, in eqtype]
EqFun.Endo.f [variable, in eqtype]
EqFun.Endo.g [variable, in eqtype]
EqFun.Endo.T [variable, in eqtype]
EqFun.f [variable, in eqtype]
EqFun.h [variable, in eqtype]
EqFun.k [variable, in eqtype]
EqFun.rT1 [variable, in eqtype]
EqFun.rT2 [variable, in eqtype]
EqImage [section, in fintype]
EqImage.T [variable, in fintype]
EqImage.T' [variable, in fintype]
EqMap [section, in seq]
EqMap.f [variable, in seq]
EqMap.Hf [variable, in seq]
EqMap.n0 [variable, in seq]
EqMap.T1 [variable, in seq]
EqMap.T2 [variable, in seq]
EqMap.x1 [variable, in seq]
EqMap.x2 [variable, in seq]
EqMask [section, in seq]
EqMask.n0 [variable, in seq]
EqMask.T [variable, in seq]
EqMixin [abbreviation, in eqtype]
eqn [definition, in ssrnat]
eqnE [lemma, in ssrnat]
eqnP [lemma, in ssrnat]
eqn0Ngt [lemma, in ssrnat]
eqn0_xor_gt0 [inductive, in ssrnat]
eqn_addl [lemma, in ssrnat]
eqn_addr [lemma, in ssrnat]
eqn_div [lemma, in div]
eqn_dvd [lemma, in div]
eqn_exp2l [lemma, in ssrnat]
eqn_exp2r [lemma, in ssrnat]
eqn_leq [lemma, in ssrnat]
eqn_maxl [lemma, in ssrnat]
eqn_maxr [lemma, in ssrnat]
eqn_minl [lemma, in ssrnat]
eqn_minr [lemma, in ssrnat]
eqn_mod_dvd [lemma, in div]
eqn_mul [lemma, in div]
eqn_mul1 [lemma, in ssrnat]
eqn_mul2l [lemma, in ssrnat]
eqn_mul2r [lemma, in ssrnat]
eqn_pmul2l [lemma, in ssrnat]
eqn_pmul2r [lemma, in ssrnat]
eqn_sqr [lemma, in ssrnat]
eqp [definition, in poly]
eqP [lemma, in eqtype]
EqPath [section, in paths]
EqPath.e [variable, in paths]
EqPath.n0 [variable, in paths]
EqPath.T [variable, in paths]
EqPath.x0_cycle [variable, in paths]
EqPmap [section, in seq]
EqPmapSub [section, in seq]
EqPmapSub.p [variable, in seq]
EqPmapSub.sT [variable, in seq]
EqPmapSub.T [variable, in seq]
EqPmap.aT [variable, in seq]
EqPmap.f [variable, in seq]
EqPmap.fK [variable, in seq]
EqPmap.g [variable, in seq]
EqPmap.rT [variable, in seq]
eqPn0 [lemma, in polydiv]
eqpP [lemma, in poly]
EqPred [section, in eqtype]
EqPred.b [variable, in eqtype]
EqPred.T [variable, in eqtype]
EqPred.u [variable, in eqtype]
EqPred.x [variable, in eqtype]
EqPred.y [variable, in eqtype]
EqPred.z [variable, in eqtype]
eqpxx [lemma, in poly]
eqp0E [lemma, in poly]
eqp1_dvd [lemma, in polydiv]
eqp1_dvd1 [lemma, in polydiv]
eqp_dvdl [lemma, in polydiv]
eqp_dvdr [lemma, in polydiv]
eqp_map [lemma, in poly]
eqp_mulC [lemma, in polydiv]
eqp_mull [lemma, in polydiv]
eqp_polyC [lemma, in polydiv]
eqp_root [lemma, in polydiv]
eqp_sym [lemma, in poly]
eqp_trans [lemma, in poly]
eqp_transl [lemma, in polydiv]
eqp_transr [lemma, in polydiv]
eqrel [definition, in ssrfun]
EqSeq [section, in seq]
eqseq [definition, in seq]
eqseqE [lemma, in seq]
eqseqP [lemma, in seq]
EqSeq.Filters [section, in seq]
EqSeq.Filters.a [variable, in seq]
EqSeq.n0 [variable, in seq]
EqSeq.T [variable, in seq]
EqSeq.x0 [variable, in seq]
eqseq_cat [lemma, in seq]
eqseq_class [definition, in seq]
eqseq_cons [lemma, in seq]
eqseq_rcons [lemma, in seq]
eqseq_rot [lemma, in seq]
eqSS [lemma, in ssrnat]
eqsVneq [lemma, in finset]
EqTheory [section, in finfun]
EqTheory.aT [variable, in finfun]
EqTheory.Partial [section, in finfun]
EqTheory.Partial.d [variable, in finfun]
EqTheory.Partial.y0 [variable, in finfun]
EqTheory.rT [variable, in finfun]
EqTrajectory [section, in paths]
EqTrajectory.f [variable, in paths]
EqTrajectory.T [variable, in paths]
EqTuple [section, in tuple]
EqTuple.n [variable, in tuple]
EqTuple.T [variable, in tuple]
EqType [abbreviation, in eqtype]
eqType [abbreviation, in eqtype]
eqtype [library]
EqTypePred [moduleid, in eqtype]
EqTypePredSig [moduleid, in eqtype]
EqTypePredSig.sort [axiom, in eqtype]
Equality [moduleid, in eqtype]
Equality.axiom [definition, in eqtype]
Equality.class [definition, in eqtype]
Equality.class_of [abbreviation, in eqtype]
Equality.clone [definition, in eqtype]
Equality.Mixin [constructor, in eqtype]
Equality.mixin_of [record, in eqtype]
Equality.op [projection, in eqtype]
Equality.Pack [constructor, in eqtype]
Equality.pack [definition, in eqtype]
Equality.sort [projection, in eqtype]
Equality.type [record, in eqtype]
equivPif [lemma, in ssrbool]
equivPifn [lemma, in ssrbool]
eqVneq [lemma, in eqtype]
eqxx [abbreviation, in eqtype]
Eq0NotPos [constructor, in ssrnat]
eq_all [lemma, in seq]
eq_all_r [lemma, in seq]
eq_axiomK [lemma, in eqtype]
eq_big [lemma, in bigops]
eq_bigl [lemma, in bigops]
eq_bigmax [lemma, in bigops]
eq_bigmax_cond [lemma, in bigops]
eq_bigr [lemma, in bigops]
eq_big_idx [lemma, in bigops]
eq_big_idx_seq [lemma, in bigops]
eq_big_op [lemma, in bigops]
eq_big_op_seq [lemma, in bigops]
eq_big_perm [lemma, in bigops]
eq_bij [lemma, in ssrfun]
eq_binP [lemma, in ssrnat]
eq_can [lemma, in ssrfun]
eq_card [lemma, in fintype]
eq_cardT [lemma, in fintype]
eq_card0 [lemma, in fintype]
eq_card1 [lemma, in fintype]
eq_card_prod [lemma, in fintype]
eq_card_sub [lemma, in fintype]
eq_card_trans [lemma, in fintype]
eq_choose [lemma, in choice]
eq_codom [lemma, in fintype]
eq_comp [lemma, in ssrfun]
eq_comparable [definition, in eqtype]
eq_connect [lemma, in connect]
eq_connect0 [lemma, in connect]
eq_count [lemma, in seq]
eq_disjoint [lemma, in fintype]
eq_disjoint0 [lemma, in fintype]
eq_disjoint1 [lemma, in fintype]
eq_disjoint_r [lemma, in fintype]
eq_enum [lemma, in fintype]
eq_existsb [lemma, in fintype]
eq_ex_maxn [lemma, in ssrnat]
eq_ex_minn [lemma, in ssrnat]
eq_fcard [lemma, in connect]
eq_fconnect [lemma, in connect]
eq_filter [lemma, in seq]
eq_find [lemma, in seq]
eq_finv [lemma, in connect]
eq_forallb [lemma, in fintype]
eq_fpath [lemma, in connect]
eq_from_nth [lemma, in seq]
eq_from_tnth [lemma, in tuple]
eq_froot [lemma, in connect]
eq_froots [lemma, in connect]
eq_has [lemma, in seq]
eq_has_r [lemma, in seq]
eq_image [lemma, in fintype]
eq_imset [lemma, in finset]
eq_inj [lemma, in ssrfun]
eq_invF [lemma, in fintype]
eq_in_filter [lemma, in seq]
eq_in_imset [lemma, in finset]
eq_in_imset2 [lemma, in finset]
eq_in_map [lemma, in seq]
eq_in_partn [lemma, in prime]
eq_in_pnat [lemma, in prime]
eq_irrelevance [lemma, in eqtype]
eq_iter [lemma, in ssrnat]
eq_iteri [lemma, in ssrnat]
eq_iterop [lemma, in ssrnat]
eq_leq [lemma, in ssrnat]
eq_map [lemma, in seq]
eq_mem [definition, in ssrbool]
eq_mkseq [lemma, in seq]
eq_negn [lemma, in prime]
eq_n_comp [lemma, in connect]
eq_n_comp_r [lemma, in connect]
eq_op [definition, in eqtype]
eq_partn [lemma, in prime]
eq_path [lemma, in paths]
eq_pick [lemma, in fintype]
eq_piP [lemma, in prime]
eq_pmap [lemma, in seq]
eq_pnat [lemma, in prime]
eq_pred1 [lemma, in connect]
eq_preimset [lemma, in finset]
eq_primes [lemma, in prime]
eq_proper [lemma, in fintype]
eq_proper_r [lemma, in fintype]
eq_refl [lemma, in eqtype]
eq_root [lemma, in connect]
eq_roots [lemma, in connect]
eq_sorted [lemma, in paths]
eq_sorted_irr [lemma, in paths]
eq_subset [lemma, in fintype]
eq_subset_r [lemma, in fintype]
eq_subxx [lemma, in fintype]
eq_sym [lemma, in eqtype]
eq_tag [lemma, in eqtype]
eq_Tagged [lemma, in eqtype]
eq_xchoose [lemma, in choice]
erefl [definition, in ssrfun]
esym [definition, in ssrfun]
esymK [lemma, in ssrfun]
etrans [definition, in ssrfun]
etrans_id [lemma, in ssrfun]
euclid [lemma, in prime]
euclid1 [lemma, in prime]
euclid_exp [lemma, in prime]
EvalPolynomial [section, in poly]
EvalPolynomial.R [variable, in poly]
eval_amulXnT [lemma, in closedfields]
eval_bigmul [abbreviation, in closedfields]
eval_lift [lemma, in closedfields]
eval_mulpT [lemma, in closedfields]
eval_natmulpT [lemma, in closedfields]
eval_opppT [lemma, in closedfields]
eval_poly [definition, in closedfields]
eval_poly1 [lemma, in closedfields]
eval_poly_mulM [lemma, in closedfields]
eval_sumpT [lemma, in closedfields]
even_prime [lemma, in prime]
ev_ax [abbreviation, in eqtype]
exchange_big [lemma, in bigops]
exchange_big_dep [lemma, in bigops]
exchange_big_dep_nat [lemma, in bigops]
exchange_big_nat [lemma, in bigops]
exFP [definition, in fintype]
existsP [lemma, in fintype]
ExMaxn [section, in ssrnat]
ExMaxnSpec [constructor, in ssrnat]
ExMaxn.exP [variable, in ssrnat]
ExMaxn.m [variable, in ssrnat]
ExMaxn.P [variable, in ssrnat]
ExMaxn.ubP [variable, in ssrnat]
ExmFalse [constructor, in ssrbool]
ExMinn [section, in ssrnat]
ExMinnSpec [constructor, in ssrnat]
ExMinn.exP [variable, in ssrnat]
ExMinn.P [variable, in ssrnat]
exmP [lemma, in ssrbool]
ExmTrue [constructor, in ssrbool]
exm_spec [inductive, in ssrbool]
expIn [lemma, in ssrnat]
expn [definition, in ssrnat]
expnE [lemma, in ssrnat]
expnI [lemma, in ssrnat]
expnS [lemma, in ssrnat]
expnSr [lemma, in ssrnat]
expn0 [lemma, in ssrnat]
expn1 [lemma, in ssrnat]
expn_add [lemma, in ssrnat]
expn_addl [definition, in binomial]
expn_eq0 [lemma, in ssrnat]
expn_gt0 [lemma, in ssrnat]
expn_mull [lemma, in ssrnat]
expn_mulr [lemma, in ssrnat]
expn_rec [definition, in ssrnat]
expn_sum [lemma, in bigops]
exp0n [lemma, in ssrnat]
exp1n [lemma, in ssrnat]
extend_number [definition, in ssrnat]
ExtensionalEquality [section, in ssrfun]
ExtensionalEquality.A [variable, in ssrfun]
ExtensionalEquality.B [variable, in ssrfun]
ExtensionalEquality.C [variable, in ssrfun]
Extensionality [section, in bigops]
Extensionality.idx [variable, in bigops]
Extensionality.op [variable, in bigops]
Extensionality.R [variable, in bigops]
Extensionality.SeqExtension [section, in bigops]
Extensionality.SeqExtension.I [variable, in bigops]
ExtraArith [section, in polydiv]
ExtraPolynomialFields [section, in polydiv]
ExtraPolynomialFields.axiom [variable, in polydiv]
ExtraPolynomialFields.F [variable, in polydiv]
ExtraPolynomialIdomain [section, in polydiv]
ExtraPolynomialIdomain.R [variable, in polydiv]
Extrema [section, in fintype]
Extrema.F [variable, in fintype]
Extrema.I [variable, in fintype]
Extrema.i0 [variable, in fintype]
Extrema.P [variable, in fintype]
Extrema.Pi0 [variable, in fintype]
ExtremumSpec [constructor, in fintype]
extremum_spec [inductive, in fintype]
ex_elim [definition, in closedfields]
ex_elim_qf [lemma, in closedfields]
ex_elim_seq [definition, in closedfields]
ex_elim_seqP [lemma, in closedfields]
ex_elim_seq_qf [lemma, in closedfields]
ex_maxn [definition, in ssrnat]
ex_maxnP [lemma, in ssrnat]
ex_maxn_spec [inductive, in ssrnat]
ex_maxn_subproof [lemma, in ssrnat]
ex_maxset [lemma, in finset]
ex_minn [definition, in ssrnat]
ex_minnP [lemma, in ssrnat]
ex_minn_spec [inductive, in ssrnat]
ex_minset [lemma, in finset]
ex_px_neq0 [lemma, in polydiv]

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)