| 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 | _ | other | (325 entries) |
| Library 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 | _ | other | (14 entries) |
| Lemma 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 | _ | other | (265 entries) |
| Constructor 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 | _ | other | (2 entries) |
| Inductive 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 | _ | other | (1 entry) |
| Abbreviation 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 | _ | other | (1 entry) |
| Definition 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 | _ | other | (42 entries) |
Global Index
A
absmodzmod [lemma, in Pocklington.modulo]abs_inj_list [lemma, in Pocklington.list]
abs_neq_lt [lemma, in Pocklington.natZ]
abs_pred_pos [lemma, in Pocklington.natZ]
abs_minus_pos [lemma, in Pocklington.natZ]
abs_plus_pos [lemma, in Pocklington.natZ]
abs_mult [lemma, in Pocklington.natZ]
abs_inj [lemma, in Pocklington.natZ]
abs_opp [lemma, in Pocklington.natZ]
allbefore [definition, in Pocklington.dec]
allbefore_ok [lemma, in Pocklington.dec]
alldec [lemma, in Pocklington.dec]
allex [definition, in Pocklington.fermat]
allex_permmod [lemma, in Pocklington.fermat]
allex_nodoubles_drop [lemma, in Pocklington.fermat]
allLinCombMod [definition, in Pocklington.pock]
allLinCombMod_ok [lemma, in Pocklington.pock]
alllincombzalllincomb [lemma, in Pocklington.pock]
alllist [definition, in Pocklington.list]
alllist_ok [lemma, in Pocklington.list]
alllist_dec [lemma, in Pocklington.list]
allPos [definition, in Pocklington.list]
allPrime [definition, in Pocklington.prime]
allprimeallzprime [lemma, in Pocklington.prime]
allZPrime [definition, in Pocklington.prime]
allzprimeallpos [lemma, in Pocklington.prime]
allzprimeallprime [lemma, in Pocklington.prime]
anddec [lemma, in Pocklington.dec]
B
bdivdec [lemma, in Pocklington.divides]bDivides [definition, in Pocklington.divides]
beq_nat_neq [lemma, in Pocklington.dec]
beq_nat_eq [lemma, in Pocklington.dec]
beq_nat_ok [lemma, in Pocklington.dec]
bPrime [definition, in Pocklington.prime]
bprimedec [lemma, in Pocklington.prime]
C
common_div [definition, in Pocklington.gcd]Cons [constructor, in Pocklington.list]
D
dec [library]decDeMorgan [lemma, in Pocklington.dec]
divbdiv [lemma, in Pocklington.divides]
divdec [lemma, in Pocklington.divides]
Divides [definition, in Pocklington.divides]
divides [library]
divmultgcd [lemma, in Pocklington.modprime]
divzdiv [lemma, in Pocklington.divides]
div_plus_r [lemma, in Pocklington.divides]
div_absexp_compat [lemma, in Pocklington.divides]
div_mult_compat_l [lemma, in Pocklington.divides]
div_minus_compat [lemma, in Pocklington.divides]
div_plus_compat [lemma, in Pocklington.divides]
div_rem0 [lemma, in Pocklington.divides]
div_rem [lemma, in Pocklington.divides]
div_le [lemma, in Pocklington.divides]
div_le1 [lemma, in Pocklington.divides]
div_antisym [lemma, in Pocklington.divides]
div_trans [lemma, in Pocklington.divides]
div_refl [lemma, in Pocklington.divides]
drop [definition, in Pocklington.list]
E
eqdec [lemma, in Pocklington.dec]eqmod [lemma, in Pocklington.modulo]
euclid_gcd [lemma, in Pocklington.gcd]
euclid_gcd1 [lemma, in Pocklington.gcd]
exbefore [definition, in Pocklington.dec]
exbefore_ok [lemma, in Pocklington.dec]
exdec [lemma, in Pocklington.dec]
exlist [definition, in Pocklington.list]
exlist_ok [lemma, in Pocklington.list]
exlist_dec [lemma, in Pocklington.list]
Exp [definition, in Pocklington.exp]
exp [library]
expzexp [lemma, in Pocklington.exp]
exp_pred_succ [lemma, in Pocklington.exp]
exp_eq [lemma, in Pocklington.exp]
exp_not0 [lemma, in Pocklington.exp]
exp_mult [lemma, in Pocklington.exp]
exp_abn [lemma, in Pocklington.exp]
exp_plus [lemma, in Pocklington.exp]
exp_S [lemma, in Pocklington.exp]
exp_1 [lemma, in Pocklington.exp]
exp_0 [lemma, in Pocklington.exp]
F
fermat [library]flt [lemma, in Pocklington.fermat]
G
gcd [definition, in Pocklington.gcd]gcd [library]
gcd_lincomb [lemma, in Pocklington.gcd]
gcd_lincomb_pos [lemma, in Pocklington.gcd]
gcd_lincomb_nat [lemma, in Pocklington.gcd]
gcd_0_r [lemma, in Pocklington.gcd]
gcd_0_l [lemma, in Pocklington.gcd]
gcd_opp_r [lemma, in Pocklington.gcd]
gcd_opp_l [lemma, in Pocklington.gcd]
gcd_sym [lemma, in Pocklington.gcd]
gcd_unq [lemma, in Pocklington.gcd]
gedec [lemma, in Pocklington.dec]
gtdec [lemma, in Pocklington.dec]
gtzgt [lemma, in Pocklington.natZ]
I
iffdec [lemma, in Pocklington.dec]impdec [lemma, in Pocklington.dec]
inj_zexp [lemma, in Pocklington.exp]
inj_abs_pos_list [lemma, in Pocklington.list]
inj_abs_neg [lemma, in Pocklington.natZ]
inj_abs_pos [lemma, in Pocklington.natZ]
inlist [definition, in Pocklington.list]
inlist_inj_abs_pos_list [lemma, in Pocklington.list]
inlist_dec [lemma, in Pocklington.list]
inlist_tail [lemma, in Pocklington.list]
inlist_head_neq [lemma, in Pocklington.list]
inlist_head_eq [lemma, in Pocklington.list]
isnat_mult [lemma, in Pocklington.natZ]
isnat_plus [lemma, in Pocklington.natZ]
isnat_abs_inj [lemma, in Pocklington.natZ]
isnat_inj_abs [lemma, in Pocklington.natZ]
istrue [definition, in Pocklington.dec]
L
ledec [lemma, in Pocklington.dec]lemmas [library]
length [definition, in Pocklington.list]
length_S [lemma, in Pocklington.list]
length_0 [lemma, in Pocklington.list]
lezle [lemma, in Pocklington.natZ]
le_diff0 [lemma, in Pocklington.lemmas]
le_le_mult [lemma, in Pocklington.lemmas]
le_witness [lemma, in Pocklington.lemmas]
le_n_nn [lemma, in Pocklington.lemmas]
le_n_mn [lemma, in Pocklington.lemmas]
le_n_nm [lemma, in Pocklington.lemmas]
le_mult_r [lemma, in Pocklington.lemmas]
le_mult_l [lemma, in Pocklington.lemmas]
LinComb [definition, in Pocklington.gcd]
LinCombMod [definition, in Pocklington.gcd]
lincombmodzlincombmod [lemma, in Pocklington.gcd]
list [inductive, in Pocklington.list]
list [library]
ltdec [lemma, in Pocklington.dec]
ltzlt [lemma, in Pocklington.natZ]
lt_multpred_pp [lemma, in Pocklington.lemmas]
lt_n_nm_m_gt_1 [lemma, in Pocklington.lemmas]
lt_lt_mult [lemma, in Pocklington.lemmas]
lt_witness [lemma, in Pocklington.lemmas]
lt_n_nm [lemma, in Pocklington.lemmas]
lt_mult_l [lemma, in Pocklington.lemmas]
lt_plus_plus [lemma, in Pocklington.lemmas]
M
Map [abbreviation, in Pocklington.list]map [definition, in Pocklington.list]
mapmult [definition, in Pocklington.list]
mapmult_orig [lemma, in Pocklington.list]
mapmult_image [lemma, in Pocklington.list]
map_length [lemma, in Pocklington.list]
Mod [definition, in Pocklington.modulo]
moda0_exp_compat [lemma, in Pocklington.modulo]
moddec [lemma, in Pocklington.modulo]
moddivmin [lemma, in Pocklington.modulo]
modpq_modp [lemma, in Pocklington.modulo]
modprime [library]
modulo [library]
modzmod [lemma, in Pocklington.modulo]
mod_not_exp_0 [lemma, in Pocklington.modprime]
mod_mult_0 [lemma, in Pocklington.modprime]
mod_mult_cancel_r [lemma, in Pocklington.modprime]
mod_mult_inv_r [lemma, in Pocklington.modprime]
mod_repr_eq [lemma, in Pocklington.modulo]
mod_repr_non_0 [lemma, in Pocklington.modulo]
mod_exp1 [lemma, in Pocklington.modulo]
mod_0not1 [lemma, in Pocklington.modulo]
mod_nx_0_n [lemma, in Pocklington.modulo]
mod_minus_compat [lemma, in Pocklington.modulo]
mod_opp_compat [lemma, in Pocklington.modulo]
mod_exp_compat [lemma, in Pocklington.modulo]
mod_sqr_compat [lemma, in Pocklington.modulo]
mod_mult_compat [lemma, in Pocklington.modulo]
mod_plus_compat [lemma, in Pocklington.modulo]
mod_trans [lemma, in Pocklington.modulo]
mod_sym [lemma, in Pocklington.modulo]
mod_refl [lemma, in Pocklington.modulo]
multDrop [definition, in Pocklington.list]
multdropzmultdrop [lemma, in Pocklington.list]
multdrop_mult [lemma, in Pocklington.list]
multdrop_cons_neq [lemma, in Pocklington.list]
multdrop_cons_eq [lemma, in Pocklington.list]
mult_pq1_p1q1 [lemma, in Pocklington.lemmas]
mult_ppq_p0q1 [lemma, in Pocklington.lemmas]
N
natlist [definition, in Pocklington.list]natZ [library]
nat_ge_0 [lemma, in Pocklington.natZ]
Nil [constructor, in Pocklington.list]
nodoubles [definition, in Pocklington.fermat]
nodoubles_allex_permmod [lemma, in Pocklington.fermat]
nodoubles_allex_permmod1 [lemma, in Pocklington.fermat]
nodoubles_ind [lemma, in Pocklington.fermat]
nodoubles_drop [lemma, in Pocklington.fermat]
nodoubles_nil [lemma, in Pocklington.fermat]
nonprime_primewitness [lemma, in Pocklington.prime]
nonprime_sqrwitness [lemma, in Pocklington.prime]
nonprime_witness [lemma, in Pocklington.prime]
notdec [lemma, in Pocklington.dec]
notdiv_rem [lemma, in Pocklington.divides]
n0n1_or_gt [lemma, in Pocklington.lemmas]
O
ordec [lemma, in Pocklington.dec]Order [definition, in Pocklington.order]
order [library]
orderdec [lemma, in Pocklington.order]
order_le_predp [lemma, in Pocklington.order]
order_div [lemma, in Pocklington.order]
order_ex [lemma, in Pocklington.order]
order_ex1 [lemma, in Pocklington.order]
P
permmod [definition, in Pocklington.fermat]permmod_drop_rev [lemma, in Pocklington.fermat]
permmod_drop_drop [lemma, in Pocklington.fermat]
permmod_drop_drop1 [lemma, in Pocklington.fermat]
permmod_trans [lemma, in Pocklington.fermat]
permmod_trans1 [lemma, in Pocklington.fermat]
permmod_allex [lemma, in Pocklington.fermat]
permmod_product [lemma, in Pocklington.fermat]
permmod_sym [lemma, in Pocklington.fermat]
permmod_refl [lemma, in Pocklington.fermat]
permmod_length [lemma, in Pocklington.fermat]
permmod_cons_extend [lemma, in Pocklington.fermat]
permmod_drop_cons [lemma, in Pocklington.fermat]
permmod_drop [lemma, in Pocklington.fermat]
permmod_nil [lemma, in Pocklington.fermat]
pock [library]
pocklington [lemma, in Pocklington.pock]
Pocklington [library]
predminus1 [lemma, in Pocklington.lemmas]
Prime [definition, in Pocklington.prime]
prime [library]
primebprime [lemma, in Pocklington.prime]
primedec [lemma, in Pocklington.prime]
primedivmult [lemma, in Pocklington.modprime]
primediv1p [lemma, in Pocklington.prime]
primepropdiv [lemma, in Pocklington.prime]
primezprime [lemma, in Pocklington.prime]
prime_div_or_gcd1 [lemma, in Pocklington.modprime]
prime2 [lemma, in Pocklington.prime]
product [definition, in Pocklington.list]
productzproduct [lemma, in Pocklington.list]
S
simpl_eq_mult_l [lemma, in Pocklington.lemmas]simpl_le_mult_l [lemma, in Pocklington.lemmas]
simpl_lt_mult_l [lemma, in Pocklington.lemmas]
sqrbound [lemma, in Pocklington.lemmas]
sqrdivbound [lemma, in Pocklington.divides]
sqr_ascend [lemma, in Pocklington.lemmas]
S_inj [lemma, in Pocklington.lemmas]
T
techlemma3 [lemma, in Pocklington.modprime]U
until [definition, in Pocklington.fermat]untiln_prod_not_0modp [lemma, in Pocklington.fermat]
until_mapmult_permmod [lemma, in Pocklington.fermat]
until_nodoubles [lemma, in Pocklington.fermat]
until_nodoubles1 [lemma, in Pocklington.fermat]
until_mapmult_allex [lemma, in Pocklington.fermat]
until_mapmult_exp [lemma, in Pocklington.fermat]
until_prod_not_0mod [lemma, in Pocklington.fermat]
until_not_0mod [lemma, in Pocklington.fermat]
until_le_n [lemma, in Pocklington.fermat]
until_pos [lemma, in Pocklington.fermat]
until_mod_all [lemma, in Pocklington.fermat]
until_ok [lemma, in Pocklington.fermat]
W
witness_le [lemma, in Pocklington.lemmas]Z
ZallLinCombMod [definition, in Pocklington.pock]ZallLinCombMod_ok [lemma, in Pocklington.pock]
zdivdec [lemma, in Pocklington.divides]
zdivdiv [lemma, in Pocklington.divides]
ZDivides [definition, in Pocklington.divides]
zdiv_rem [lemma, in Pocklington.divides]
zdiv_mult_compat_l [lemma, in Pocklington.divides]
zdiv_plus_compat [lemma, in Pocklington.divides]
zdiv_plus_r [lemma, in Pocklington.divides]
zdrop [definition, in Pocklington.list]
zdrop_product [lemma, in Pocklington.list]
zdrop_inlist_swap [lemma, in Pocklington.list]
zdrop_swap [lemma, in Pocklington.list]
zdrop_inlist_weak [lemma, in Pocklington.list]
zdrop_neq_inlist [lemma, in Pocklington.list]
zdrop_length [lemma, in Pocklington.list]
zdrop_head_neq [lemma, in Pocklington.list]
zdrop_head_eq [lemma, in Pocklington.list]
zeqdec [lemma, in Pocklington.dec]
zeqmod [lemma, in Pocklington.modulo]
zeq_bool_neq [lemma, in Pocklington.dec]
zeq_bool_eq [lemma, in Pocklington.dec]
ZExp [definition, in Pocklington.exp]
zexp_mult [lemma, in Pocklington.exp]
zexp_plus [lemma, in Pocklington.exp]
zexp_S [lemma, in Pocklington.exp]
zexp_S1 [lemma, in Pocklington.exp]
zexp_eq [lemma, in Pocklington.exp]
zexp_pred_succ [lemma, in Pocklington.exp]
Zgt_neq [lemma, in Pocklington.lemmas]
Zle_mult_l [lemma, in Pocklington.lemmas]
Zle_minus [lemma, in Pocklington.lemmas]
ZLinCombMod [definition, in Pocklington.gcd]
zlincombmodlincombmod [lemma, in Pocklington.gcd]
Zlist [definition, in Pocklington.list]
Zlt_mult_l [lemma, in Pocklington.lemmas]
Zlt_neq [lemma, in Pocklington.lemmas]
ZMod [definition, in Pocklington.modulo]
zmoda0_exp_compat [lemma, in Pocklington.modulo]
zmoddec [lemma, in Pocklington.modulo]
zmoddivmin [lemma, in Pocklington.modulo]
zmodmod [lemma, in Pocklington.modulo]
zmodpq_modp [lemma, in Pocklington.modulo]
zmod_repr_non_0 [lemma, in Pocklington.modulo]
zmod_0not1 [lemma, in Pocklington.modulo]
zmod_nx_0_n [lemma, in Pocklington.modulo]
zmod_minus_compat [lemma, in Pocklington.modulo]
zmod_opp_compat [lemma, in Pocklington.modulo]
zmod_exp_compat [lemma, in Pocklington.modulo]
zmod_sqr_compat [lemma, in Pocklington.modulo]
zmod_mult_compat [lemma, in Pocklington.modulo]
zmod_plus_compat [lemma, in Pocklington.modulo]
zmod_trans [lemma, in Pocklington.modulo]
zmod_sym [lemma, in Pocklington.modulo]
zmod_refl [lemma, in Pocklington.modulo]
zmultDrop [definition, in Pocklington.list]
zmultdrop_mult [lemma, in Pocklington.list]
zmultdrop_cons_neq [lemma, in Pocklington.list]
zmultdrop_cons_eq [lemma, in Pocklington.list]
Zmult_ab0a0b0 [lemma, in Pocklington.lemmas]
Zopp_lt_gt_0 [lemma, in Pocklington.lemmas]
Zpocklington [lemma, in Pocklington.pock]
ZPrime [definition, in Pocklington.prime]
zprimeprime [lemma, in Pocklington.prime]
zprime2 [lemma, in Pocklington.prime]
zprime2a [lemma, in Pocklington.prime]
zproduct [definition, in Pocklington.list]
zproductproduct [lemma, in Pocklington.list]
Library Index
D
decdivides
E
expF
fermatG
gcdL
lemmaslist
M
modprimemodulo
N
natZO
orderP
pockPocklington
prime
Lemma Index
A
absmodzmod [in Pocklington.modulo]abs_inj_list [in Pocklington.list]
abs_neq_lt [in Pocklington.natZ]
abs_pred_pos [in Pocklington.natZ]
abs_minus_pos [in Pocklington.natZ]
abs_plus_pos [in Pocklington.natZ]
abs_mult [in Pocklington.natZ]
abs_inj [in Pocklington.natZ]
abs_opp [in Pocklington.natZ]
allbefore_ok [in Pocklington.dec]
alldec [in Pocklington.dec]
allex_permmod [in Pocklington.fermat]
allex_nodoubles_drop [in Pocklington.fermat]
allLinCombMod_ok [in Pocklington.pock]
alllincombzalllincomb [in Pocklington.pock]
alllist_ok [in Pocklington.list]
alllist_dec [in Pocklington.list]
allprimeallzprime [in Pocklington.prime]
allzprimeallpos [in Pocklington.prime]
allzprimeallprime [in Pocklington.prime]
anddec [in Pocklington.dec]
B
bdivdec [in Pocklington.divides]beq_nat_neq [in Pocklington.dec]
beq_nat_eq [in Pocklington.dec]
beq_nat_ok [in Pocklington.dec]
bprimedec [in Pocklington.prime]
D
decDeMorgan [in Pocklington.dec]divbdiv [in Pocklington.divides]
divdec [in Pocklington.divides]
divmultgcd [in Pocklington.modprime]
divzdiv [in Pocklington.divides]
div_plus_r [in Pocklington.divides]
div_absexp_compat [in Pocklington.divides]
div_mult_compat_l [in Pocklington.divides]
div_minus_compat [in Pocklington.divides]
div_plus_compat [in Pocklington.divides]
div_rem0 [in Pocklington.divides]
div_rem [in Pocklington.divides]
div_le [in Pocklington.divides]
div_le1 [in Pocklington.divides]
div_antisym [in Pocklington.divides]
div_trans [in Pocklington.divides]
div_refl [in Pocklington.divides]
E
eqdec [in Pocklington.dec]eqmod [in Pocklington.modulo]
euclid_gcd [in Pocklington.gcd]
euclid_gcd1 [in Pocklington.gcd]
exbefore_ok [in Pocklington.dec]
exdec [in Pocklington.dec]
exlist_ok [in Pocklington.list]
exlist_dec [in Pocklington.list]
expzexp [in Pocklington.exp]
exp_pred_succ [in Pocklington.exp]
exp_eq [in Pocklington.exp]
exp_not0 [in Pocklington.exp]
exp_mult [in Pocklington.exp]
exp_abn [in Pocklington.exp]
exp_plus [in Pocklington.exp]
exp_S [in Pocklington.exp]
exp_1 [in Pocklington.exp]
exp_0 [in Pocklington.exp]
F
flt [in Pocklington.fermat]G
gcd_lincomb [in Pocklington.gcd]gcd_lincomb_pos [in Pocklington.gcd]
gcd_lincomb_nat [in Pocklington.gcd]
gcd_0_r [in Pocklington.gcd]
gcd_0_l [in Pocklington.gcd]
gcd_opp_r [in Pocklington.gcd]
gcd_opp_l [in Pocklington.gcd]
gcd_sym [in Pocklington.gcd]
gcd_unq [in Pocklington.gcd]
gedec [in Pocklington.dec]
gtdec [in Pocklington.dec]
gtzgt [in Pocklington.natZ]
I
iffdec [in Pocklington.dec]impdec [in Pocklington.dec]
inj_zexp [in Pocklington.exp]
inj_abs_pos_list [in Pocklington.list]
inj_abs_neg [in Pocklington.natZ]
inj_abs_pos [in Pocklington.natZ]
inlist_inj_abs_pos_list [in Pocklington.list]
inlist_dec [in Pocklington.list]
inlist_tail [in Pocklington.list]
inlist_head_neq [in Pocklington.list]
inlist_head_eq [in Pocklington.list]
isnat_mult [in Pocklington.natZ]
isnat_plus [in Pocklington.natZ]
isnat_abs_inj [in Pocklington.natZ]
isnat_inj_abs [in Pocklington.natZ]
L
ledec [in Pocklington.dec]length_S [in Pocklington.list]
length_0 [in Pocklington.list]
lezle [in Pocklington.natZ]
le_diff0 [in Pocklington.lemmas]
le_le_mult [in Pocklington.lemmas]
le_witness [in Pocklington.lemmas]
le_n_nn [in Pocklington.lemmas]
le_n_mn [in Pocklington.lemmas]
le_n_nm [in Pocklington.lemmas]
le_mult_r [in Pocklington.lemmas]
le_mult_l [in Pocklington.lemmas]
lincombmodzlincombmod [in Pocklington.gcd]
ltdec [in Pocklington.dec]
ltzlt [in Pocklington.natZ]
lt_multpred_pp [in Pocklington.lemmas]
lt_n_nm_m_gt_1 [in Pocklington.lemmas]
lt_lt_mult [in Pocklington.lemmas]
lt_witness [in Pocklington.lemmas]
lt_n_nm [in Pocklington.lemmas]
lt_mult_l [in Pocklington.lemmas]
lt_plus_plus [in Pocklington.lemmas]
M
mapmult_orig [in Pocklington.list]mapmult_image [in Pocklington.list]
map_length [in Pocklington.list]
moda0_exp_compat [in Pocklington.modulo]
moddec [in Pocklington.modulo]
moddivmin [in Pocklington.modulo]
modpq_modp [in Pocklington.modulo]
modzmod [in Pocklington.modulo]
mod_not_exp_0 [in Pocklington.modprime]
mod_mult_0 [in Pocklington.modprime]
mod_mult_cancel_r [in Pocklington.modprime]
mod_mult_inv_r [in Pocklington.modprime]
mod_repr_eq [in Pocklington.modulo]
mod_repr_non_0 [in Pocklington.modulo]
mod_exp1 [in Pocklington.modulo]
mod_0not1 [in Pocklington.modulo]
mod_nx_0_n [in Pocklington.modulo]
mod_minus_compat [in Pocklington.modulo]
mod_opp_compat [in Pocklington.modulo]
mod_exp_compat [in Pocklington.modulo]
mod_sqr_compat [in Pocklington.modulo]
mod_mult_compat [in Pocklington.modulo]
mod_plus_compat [in Pocklington.modulo]
mod_trans [in Pocklington.modulo]
mod_sym [in Pocklington.modulo]
mod_refl [in Pocklington.modulo]
multdropzmultdrop [in Pocklington.list]
multdrop_mult [in Pocklington.list]
multdrop_cons_neq [in Pocklington.list]
multdrop_cons_eq [in Pocklington.list]
mult_pq1_p1q1 [in Pocklington.lemmas]
mult_ppq_p0q1 [in Pocklington.lemmas]
N
nat_ge_0 [in Pocklington.natZ]nodoubles_allex_permmod [in Pocklington.fermat]
nodoubles_allex_permmod1 [in Pocklington.fermat]
nodoubles_ind [in Pocklington.fermat]
nodoubles_drop [in Pocklington.fermat]
nodoubles_nil [in Pocklington.fermat]
nonprime_primewitness [in Pocklington.prime]
nonprime_sqrwitness [in Pocklington.prime]
nonprime_witness [in Pocklington.prime]
notdec [in Pocklington.dec]
notdiv_rem [in Pocklington.divides]
n0n1_or_gt [in Pocklington.lemmas]
O
ordec [in Pocklington.dec]orderdec [in Pocklington.order]
order_le_predp [in Pocklington.order]
order_div [in Pocklington.order]
order_ex [in Pocklington.order]
order_ex1 [in Pocklington.order]
P
permmod_drop_rev [in Pocklington.fermat]permmod_drop_drop [in Pocklington.fermat]
permmod_drop_drop1 [in Pocklington.fermat]
permmod_trans [in Pocklington.fermat]
permmod_trans1 [in Pocklington.fermat]
permmod_allex [in Pocklington.fermat]
permmod_product [in Pocklington.fermat]
permmod_sym [in Pocklington.fermat]
permmod_refl [in Pocklington.fermat]
permmod_length [in Pocklington.fermat]
permmod_cons_extend [in Pocklington.fermat]
permmod_drop_cons [in Pocklington.fermat]
permmod_drop [in Pocklington.fermat]
permmod_nil [in Pocklington.fermat]
pocklington [in Pocklington.pock]
predminus1 [in Pocklington.lemmas]
primebprime [in Pocklington.prime]
primedec [in Pocklington.prime]
primedivmult [in Pocklington.modprime]
primediv1p [in Pocklington.prime]
primepropdiv [in Pocklington.prime]
primezprime [in Pocklington.prime]
prime_div_or_gcd1 [in Pocklington.modprime]
prime2 [in Pocklington.prime]
productzproduct [in Pocklington.list]
S
simpl_eq_mult_l [in Pocklington.lemmas]simpl_le_mult_l [in Pocklington.lemmas]
simpl_lt_mult_l [in Pocklington.lemmas]
sqrbound [in Pocklington.lemmas]
sqrdivbound [in Pocklington.divides]
sqr_ascend [in Pocklington.lemmas]
S_inj [in Pocklington.lemmas]
T
techlemma3 [in Pocklington.modprime]U
untiln_prod_not_0modp [in Pocklington.fermat]until_mapmult_permmod [in Pocklington.fermat]
until_nodoubles [in Pocklington.fermat]
until_nodoubles1 [in Pocklington.fermat]
until_mapmult_allex [in Pocklington.fermat]
until_mapmult_exp [in Pocklington.fermat]
until_prod_not_0mod [in Pocklington.fermat]
until_not_0mod [in Pocklington.fermat]
until_le_n [in Pocklington.fermat]
until_pos [in Pocklington.fermat]
until_mod_all [in Pocklington.fermat]
until_ok [in Pocklington.fermat]
W
witness_le [in Pocklington.lemmas]Z
ZallLinCombMod_ok [in Pocklington.pock]zdivdec [in Pocklington.divides]
zdivdiv [in Pocklington.divides]
zdiv_rem [in Pocklington.divides]
zdiv_mult_compat_l [in Pocklington.divides]
zdiv_plus_compat [in Pocklington.divides]
zdiv_plus_r [in Pocklington.divides]
zdrop_product [in Pocklington.list]
zdrop_inlist_swap [in Pocklington.list]
zdrop_swap [in Pocklington.list]
zdrop_inlist_weak [in Pocklington.list]
zdrop_neq_inlist [in Pocklington.list]
zdrop_length [in Pocklington.list]
zdrop_head_neq [in Pocklington.list]
zdrop_head_eq [in Pocklington.list]
zeqdec [in Pocklington.dec]
zeqmod [in Pocklington.modulo]
zeq_bool_neq [in Pocklington.dec]
zeq_bool_eq [in Pocklington.dec]
zexp_mult [in Pocklington.exp]
zexp_plus [in Pocklington.exp]
zexp_S [in Pocklington.exp]
zexp_S1 [in Pocklington.exp]
zexp_eq [in Pocklington.exp]
zexp_pred_succ [in Pocklington.exp]
Zgt_neq [in Pocklington.lemmas]
Zle_mult_l [in Pocklington.lemmas]
Zle_minus [in Pocklington.lemmas]
zlincombmodlincombmod [in Pocklington.gcd]
Zlt_mult_l [in Pocklington.lemmas]
Zlt_neq [in Pocklington.lemmas]
zmoda0_exp_compat [in Pocklington.modulo]
zmoddec [in Pocklington.modulo]
zmoddivmin [in Pocklington.modulo]
zmodmod [in Pocklington.modulo]
zmodpq_modp [in Pocklington.modulo]
zmod_repr_non_0 [in Pocklington.modulo]
zmod_0not1 [in Pocklington.modulo]
zmod_nx_0_n [in Pocklington.modulo]
zmod_minus_compat [in Pocklington.modulo]
zmod_opp_compat [in Pocklington.modulo]
zmod_exp_compat [in Pocklington.modulo]
zmod_sqr_compat [in Pocklington.modulo]
zmod_mult_compat [in Pocklington.modulo]
zmod_plus_compat [in Pocklington.modulo]
zmod_trans [in Pocklington.modulo]
zmod_sym [in Pocklington.modulo]
zmod_refl [in Pocklington.modulo]
zmultdrop_mult [in Pocklington.list]
zmultdrop_cons_neq [in Pocklington.list]
zmultdrop_cons_eq [in Pocklington.list]
Zmult_ab0a0b0 [in Pocklington.lemmas]
Zopp_lt_gt_0 [in Pocklington.lemmas]
Zpocklington [in Pocklington.pock]
zprimeprime [in Pocklington.prime]
zprime2 [in Pocklington.prime]
zprime2a [in Pocklington.prime]
zproductproduct [in Pocklington.list]
Constructor Index
C
Cons [in Pocklington.list]N
Nil [in Pocklington.list]Inductive Index
L
list [in Pocklington.list]Abbreviation Index
M
Map [in Pocklington.list]Definition Index
A
allbefore [in Pocklington.dec]allex [in Pocklington.fermat]
allLinCombMod [in Pocklington.pock]
alllist [in Pocklington.list]
allPos [in Pocklington.list]
allPrime [in Pocklington.prime]
allZPrime [in Pocklington.prime]
B
bDivides [in Pocklington.divides]bPrime [in Pocklington.prime]
C
common_div [in Pocklington.gcd]D
Divides [in Pocklington.divides]drop [in Pocklington.list]
E
exbefore [in Pocklington.dec]exlist [in Pocklington.list]
Exp [in Pocklington.exp]
G
gcd [in Pocklington.gcd]I
inlist [in Pocklington.list]istrue [in Pocklington.dec]
L
length [in Pocklington.list]LinComb [in Pocklington.gcd]
LinCombMod [in Pocklington.gcd]
M
map [in Pocklington.list]mapmult [in Pocklington.list]
Mod [in Pocklington.modulo]
multDrop [in Pocklington.list]
N
natlist [in Pocklington.list]nodoubles [in Pocklington.fermat]
O
Order [in Pocklington.order]P
permmod [in Pocklington.fermat]Prime [in Pocklington.prime]
product [in Pocklington.list]
U
until [in Pocklington.fermat]Z
ZallLinCombMod [in Pocklington.pock]ZDivides [in Pocklington.divides]
zdrop [in Pocklington.list]
ZExp [in Pocklington.exp]
ZLinCombMod [in Pocklington.gcd]
Zlist [in Pocklington.list]
ZMod [in Pocklington.modulo]
zmultDrop [in Pocklington.list]
ZPrime [in Pocklington.prime]
zproduct [in Pocklington.list]
| 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 | _ | other | (325 entries) |
| Library 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 | _ | other | (14 entries) |
| Lemma 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 | _ | other | (265 entries) |
| Constructor 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 | _ | other | (2 entries) |
| Inductive 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 | _ | other | (1 entry) |
| Abbreviation 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 | _ | other | (1 entry) |
| Definition 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 | _ | other | (42 entries) |