Global Index

J

K

W

X

Y

_

(687 entries)

Axiom Index

A

B

C

F

G

H

J

K

L

R

S

T

V

W

X

Y

Z

_

(25 entries)

Lemma Index

J

K

Q

U

W

X

Y

_

(497 entries)

Constructor Index

A

B

D

G

J

K

M

O

Q

U

W

X

Y

Z

_

(50 entries)

Inductive Index

A

B

D

G

J

K

M

O

Q

U

V

W

X

Y

Z

_

(25 entries)

Definition Index

B

J

K

O

Q

R

U

V

W

X

Y

_

(60 entries)

Library Index

B

F

G

J

K

Q

V

W

X

Y

Z

_

(30 entries)

Global Index

A

add_effic [lemma, in prueba_tes]
add_effic_cor_l [lemma, in prueba_tes]
add_effic_full [lemma, in prueba_tes]
add_effic_fun [definition, in prueba_tes]
asoc_mon_pol [lemma, in Somme_poly_tes]
asoc_suma [lemma, in Somme_poly_tes]
auxiliar2 [lemma, in orden_pol]
aux1_hterm_eq_suma_Ttm [lemma, in Hmtc]
aux1_hterm_suma_Ttm [lemma, in Hmtc]
aux1_red_menor2 [lemma, in noetred_tes]
aux2_hterm_eq_suma_Ttm [lemma, in Hmtc]
aux2_red_menor2 [lemma, in noetred_tes]
aux_hterm_suma_Ttm [lemma, in Hmtc]
aux_no_hterm_Ttm_in_red [lemma, in Hmtc_axiom]
aux_suma_app_full [lemma, in pol_can]
Axiomas_n_full2_tes [library]
ayuda_Benj [lemma, in ecuaciones_tes]
ayuda_full_imp_lis_desc [lemma, in orden_pol]
ayud_Gilb [lemma, in ecuaciones_tes]

B

basic2 [lemma, in red_expl]
basic2_bis [lemma, in red_expl]
basic3 [lemma, in red_expl]
basic3_full [lemma, in impl_large]
basic4 [lemma, in red_expl]
basic4_full [lemma, in impl_large]
buen_ord_red [lemma, in noetred_tes]
buen_ord_red1 [lemma, in noetred_tes]

C

calcula_fnbis [lemma, in normal_tes]
can_corr [lemma, in pol_can]
can_fun [lemma, in pol_can]
can_is_full [lemma, in pol_can]
caseRed1xy [lemma, in ult_impl]
ch_m_plus [lemma, in ecuaciones_tes]
ch_m_plus2 [lemma, in ecuaciones_tes]
coef [definition, in coeficiente_tes]
coeficiente_tes [library]
coef_first [lemma, in pol_can]
coef_hterm [lemma, in Hmtc]
coef_low_pol [lemma, in pol_can]
coef_n_term [lemma, in coeficiente_tes]
coef_pol_opp [lemma, in coeficiente_tes]
coef_pol_opp2 [lemma, in coeficiente_tes]
coef_suma_pol [lemma, in coeficiente_tes]
coef_suma_Ttm [lemma, in Hmtc]
coef_term_mult [lemma, in coeficiente_tes]
coef_Ttm_split_pol [lemma, in coeficiente_tes]
coef_z_in_pol [lemma, in coeficiente_tes]
common_is_Red_equiv [lemma, in lemma_cong_red2_tes]
common_succ [inductive, in lemma_cong_red2_tes]
common_succ_full [inductive, in S_poly_nuevo2_tes]
common_succ_red [constructor, in lemma_cong_red2_tes]
common_succ_red_full [constructor, in S_poly_nuevo2_tes]
common_succ_step [inductive, in lemma_cong_red2_tes]
common_succ_step_red [constructor, in lemma_cong_red2_tes]
comm_mult_can [lemma, in pol_can]
comp_common_succ [lemma, in Axiomas_n_full2_tes]
comp_common_succ_full [lemma, in S_poly_nuevo2_tes]
comp_divis_lex [lemma, in divisib_tes]
comp_mult_m_effic [lemma, in prueba_tes]
comp_mult_p_effic [lemma, in prueba_tes]
comp_nOQ [lemma, in Corps_tes]
comp_no_term_in_pol [lemma, in coeficiente_tes]
comp_sum_effic [lemma, in prueba_tes]
comp_term_in_pol [lemma, in coeficiente_tes]
cond_ht_pol [lemma, in Hmtc]
confluente [definition, in S_poly_nuevo2_tes]
confluente_full [definition, in S_poly_nuevo2_tes]
congr_conv [lemma, in Axiomas_n_full2_tes]
congr_y_red2_tes [library]
conmt_common_succ [lemma, in lemma_cong_red2_tes]
conmt_common_succ_full [lemma, in S_poly_nuevo2_tes]
conmt_suma [lemma, in Somme_poly_tes]
cons_full_fam [lemma, in reduccion2_tes]
contr_hterm_vpol [lemma, in Hmtc]
contr_mult_nz_monom [lemma, in Div_poly_tes]
conv_congr [lemma, in congr_y_red2_tes]
con_red_cong [lemma, in congr_y_red2_tes]
Corps_tes [library]
cpol [constructor, in Polynomes_tes]
cr_full [lemma, in S_poly_nuevo2_tes]

D

decQ [axiom, in Corps_tes]
decQ_t [lemma, in Corps_tes]
dec_coef_monom [lemma, in Monomes_tes]
dec_sum_term_in_pol [lemma, in coeficiente_tes]
dec_term_div [lemma, in divisib_tes]
dec_term_in_pol [lemma, in coeficiente_tes]
Desc_rev [lemma, in orden_pol]
Desc_rev_pol [lemma, in orden_pol]
Diagrama [lemma, in ult_impl]
distrQ [axiom, in Corps_tes]
distr_divQ [lemma, in Corps_tes]
distr_div_suma [lemma, in Div_poly_tes]
distr_mult_m_monom [lemma, in Mult_poly_tes]
distr_mult_p [lemma, in Mult_poly_tes]
distr_mult_p_r [lemma, in Mult_poly_tes]
divisib_tes [library]
division [lemma, in Corps_tes]
divis_im_divt [lemma, in divisib_tes]
divQ [definition, in Corps_tes]
divQ_0 [lemma, in Corps_tes]
divQ_0_n [lemma, in Corps_tes]
div_lcm1 [lemma, in Lcm_tes]
div_lcm2 [lemma, in Lcm_tes]
div_m [definition, in Div_poly_tes]
div_mon [definition, in Monomes_tes]
div_mult_inv [lemma, in Div_poly_tes]
div_mult_mon_inv [lemma, in divisib_tes]
div_pm_comp [lemma, in Div_poly_tes]
Div_poly_tes [library]
div_Q_eq [lemma, in Corps_tes]
div_term [definition, in divisib_tes]
div_term_hterm [lemma, in Hmtc]
div_trans [lemma, in divisib_tes]

E

ecuaciones_tes [library]
ec_invQ [lemma, in Corps_tes]
eg_denomQ [lemma, in Corps_tes]
eg_denom_term [lemma, in divisib_tes]
eg_numeraQ [lemma, in Corps_tes]
elem_full [lemma, in reduccion2_tes]
elem_n_vpol [lemma, in reduccion2_tes]
elim_red_exp [lemma, in reduccion2_tes]
eqexp_cons [lemma, in Termes_tes]
eqQ [axiom, in Corps_tes]
eqQ_refl [axiom, in Corps_tes]
eqQ_sym [axiom, in Corps_tes]
eqQ_trans [axiom, in Corps_tes]
eqterm_cons1 [lemma, in Termes_tes]
equat1 [lemma, in ecuaciones_tes]
equat_equiv_Id [lemma, in nueva_equiv2_tes]
equiv_Id [inductive, in congr_y_red2_tes]
equiv_Id2_equiv_Id [lemma, in nueva_equiv2_tes]
equiv_Id_cons [constructor, in congr_y_red2_tes]
equiv_Id_cpol [lemma, in nueva_equiv2_tes]
equiv_Id_equiv_Id2 [lemma, in nueva_equiv2_tes]
equiv_id_trans [lemma, in congr_y_red2_tes]
equiv_m [lemma, in nueva_equiv2_tes]
equm [inductive, in Hmtc]
equmon [definition, in Monomes_tes]
equmoni [constructor, in Hmtc]
equmon_cons [lemma, in Somme_poly_tes]
equmon_refl [lemma, in Monomes_tes]
equmon_sym [lemma, in Monomes_tes]
equmon_trans [lemma, in Monomes_tes]
equmon_z [lemma, in Monomes_tes]
equm_full_hmonom [lemma, in Hmtc]
equm_refl [lemma, in Hmtc]
equm_sym [lemma, in Hmtc]
equm_trans [lemma, in Hmtc]
equpol [inductive, in Somme_poly_tes]
equpol_can [lemma, in Hmtc]
equpol_cm [constructor, in Somme_poly_tes]
equpol_cpol [lemma, in Somme_poly_tes]
equpol_cpol2 [lemma, in Somme_poly_tes]
equpol_dec_full_term [lemma, in pol_can]
equpol_elim [constructor, in Somme_poly_tes]
equpol_fn [lemma, in normal_tes]
equpol_Id_sum2 [lemma, in nueva_equiv2_tes]
equpol_Id_sum2_op [lemma, in nueva_equiv2_tes]
equpol_refl [constructor, in Somme_poly_tes]
equpol_smt [constructor, in Somme_poly_tes]
equpol_ss [constructor, in Somme_poly_tes]
equpol_sym [constructor, in Somme_poly_tes]
equpol_tran [constructor, in Somme_poly_tes]
eq_coef_monom [lemma, in Hmtc]
eq_cpol [lemma, in Somme_poly_tes]
eq_hcoef [lemma, in Hmtc]
eq_homnom_fst [lemma, in Hmtc]
eq_hterm [lemma, in Hmtc]
eq_Ideal [definition, in ideal_tes]
eq_Ideal_eq_p [lemma, in ideal_tes]
eq_mon_cpol [lemma, in Somme_poly_tes]
eq_mulQ_neg [lemma, in Corps_tes]
eq_nvpol [lemma, in Somme_poly_tes]
eq_pol_opp_hcoef [lemma, in Hmtc]
eq_pol_opp_hterm [lemma, in Hmtc]
eq_pol_opp_no_zero [lemma, in Somme_poly_tes]
eq_Red_equiv_common [lemma, in Axiomas_n_full2_tes]
eq_term_div [lemma, in Hmtc]
eq_term_in_pol_monom [lemma, in coeficiente_tes]
eq_tm_dec [lemma, in Termes_tes]
ext_full_Tpol [lemma, in orden_pol]
ext_l_Tpol_Lex3 [lemma, in orden_pol]
ext_r_Tpol_Lex3 [lemma, in orden_pol]
ex_fpol [lemma, in orden_pol]
ex_fpol_eq [lemma, in orden_pol]
ex_op [axiom, in Corps_tes]
ex_term_div_n [lemma, in divisib_tes]

F

fn_equpol_vpol [lemma, in normal_tes]
fn_p_id [lemma, in normal_tes]
For_all_cs [constructor, in reduccion2_tes]
for_all_list_pol [inductive, in reduccion2_tes]
For_all_nil [constructor, in reduccion2_tes]
for_norm [definition, in normal_tes]
for_norm_dec_vpol [lemma, in normal_tes]
fst_equm [lemma, in Hmtc]
fst_mult [lemma, in Hmtc]
fst_term [definition, in Hmtc]
full [definition, in Termes_tes]
fullp_impl_fullt [lemma, in pol_can]
full_coef [lemma, in coeficiente_tes]
full_cp_neq_vp [lemma, in pol_can]
full_eq_vpol [lemma, in pol_can]
full_fam [definition, in reduccion2_tes]
full_fam_dec [lemma, in reduccion2_tes]
full_hcoef [lemma, in Hmtc]
full_hterm [lemma, in Hmtc]
full_hterm_full_pol [lemma, in Hmtc]
full_imp_lis_desc [lemma, in orden_pol]
full_mon [definition, in Monomes_tes]
full_monom [lemma, in pol_can]
full_mult_m [lemma, in Mult_poly_tes]
full_mult_mon [lemma, in pol_can]
full_no_term [lemma, in pol_can]
full_O [lemma, in Termes_tes]
full_opp [lemma, in pol_can]
full_pol [inductive, in pol_can]
full_pol_cons [constructor, in pol_can]
full_pol_cons_term [lemma, in pol_can]
full_pol_In_hterm [lemma, in reduccion2_tes]
full_pol_mon [lemma, in pol_can]
full_pol_nil [constructor, in pol_can]
full_pol_tm_dec [lemma, in Polynomes_tes]
full_pred1 [lemma, in Termes_tes]
full_S [lemma, in Termes_tes]
full_same [lemma, in pol_can]
full_term_cpol [lemma, in Polynomes_tes]
full_term_full_fam [lemma, in reduccion2_tes]
full_term_mult_p [lemma, in Mult_poly_tes]
full_term_norm [lemma, in normal_tes]
full_term_opp [lemma, in Somme_poly_tes]
full_term_pol [inductive, in Polynomes_tes]
full_term_pol_cons [constructor, in Polynomes_tes]
full_term_pol_mon [lemma, in Polynomes_tes]
full_term_pol_nil [constructor, in Polynomes_tes]
full_term_suma_app [lemma, in Somme_poly_tes]
full_term_S_pol [lemma, in S_poly_nuevo2_tes]
full_tm_dec [lemma, in Polynomes_tes]
full_Ttm_pol_hterm [lemma, in Hmtc]
funcanvpol [lemma, in Hmtc]
fun_can [definition, in pol_can]

G

gen_split_pol [lemma, in coeficiente_tes]
Groebner1_full [definition, in S_poly_nuevo2_tes]
Groebner2_full [definition, in S_poly_nuevo2_tes]
Groebner3_CR_full [definition, in S_poly_nuevo2_tes]
Groebner3_full [definition, in S_poly_nuevo2_tes]
gr_ht_nvpol [lemma, in Hmtc]
G1_impl_G2_full [lemma, in S_poly_nuevo2_tes]
G2_impl_G1_full [lemma, in ult_impl]
G2_impl_G3_LCR_full [lemma, in impl_large]
G3CR_L_impl_G3CR_full [lemma, in ult_impl]
G3_CR_impl_G1_full [lemma, in S_poly_nuevo2_tes]
G3_CR_impl_G3_full [lemma, in S_poly_nuevo2_tes]

H

hcoef [definition, in Hmtc]
hcoef_mult [lemma, in Hmtc]
hcoef_mult2 [lemma, in Hmtc]
hcoef_no_eq_hterm [lemma, in Hmtc]
hcoef_pol_opp [lemma, in Hmtc]
hcoef_pol_opp_term [lemma, in Hmtc]
hcoef_suma_Ttm [lemma, in Hmtc]
hcoef_vpol [lemma, in Hmtc]
hmct_Leib [lemma, in Hmtc]
hmonom [definition, in Hmtc]
hmonom_mult [lemma, in Hmtc]
Hmtc [library]
Hmtc_axiom [library]
hred [inductive, in reduccion2_tes]
hred1_simpl [constructor, in reduccion2_tes]
hred_suma [lemma, in red_expl]
hred_suma_bis [lemma, in red_expl]
hterm [definition, in Hmtc]
hterm_eq_suma_Ttm [lemma, in Hmtc]
hterm_mult_m [lemma, in Hmtc]
hterm_mult_m2 [lemma, in Hmtc]
hterm_pol_m_opp [lemma, in Hmtc]
hterm_pol_opp [lemma, in Hmtc]
hterm_pol_opp_term [lemma, in Hmtc]
hterm_suma_Ttm [lemma, in Hmtc]
hterm_vpol [lemma, in Hmtc]

I

Ideal [inductive, in ideal_tes]
ideal_cpol [constructor, in ideal_tes]
Ideal_ens [definition, in ideal_tes]
ideal_mon [lemma, in ideal_tes]
ideal_suma_pol_mon [lemma, in nueva_equiv2_tes]
ideal_tes [library]
ideal_vpol [constructor, in ideal_tes]
id_trans [lemma, in ideal_tes]
igual [lemma, in Corps_tes]
impl_large [library]
imp_equiv_Id2_opp [lemma, in nueva_equiv2_tes]
inc [definition, in orden_pol]
inc_list [definition, in orden_pol]
inc_red [definition, in noetred_tes]
inc_Red1 [definition, in noetred_tes]
Ind_prueba [lemma, in ult_impl]
insert [lemma, in pol_can]
invQ [axiom, in Corps_tes]
inv_divQ [axiom, in Corps_tes]

L

lcm [definition, in Lcm_tes]
lcm_conm [lemma, in Lcm_tes]
lcm_div [lemma, in Lcm_tes]
lcm_div2 [lemma, in Lcm_tes]
lcm_full [lemma, in Lcm_tes]
Lcm_tes [library]
lcm_1 [lemma, in Lcm_tes]
lcm_2 [lemma, in Lcm_tes]
lemma_cong_red2_tes [library]
length_n_term_O [lemma, in Termes_tes]
Listterm_desc [definition, in orden_pol]
list_indlg [lemma, in orden_term]
local_confluente_full [definition, in ult_impl]
low_cons [constructor, in pol_can]
low_nil [constructor, in pol_can]
low_opp [lemma, in pol_can]
low_pol [inductive, in pol_can]
low_pol_cpol [lemma, in pol_can]
low_pol_term_mult [lemma, in pol_can]
low_trans [lemma, in pol_can]
Low_Ttm_tran [lemma, in pol_can]

M

max_num [definition, in Lcm_tes]
max_numO [lemma, in Lcm_tes]
max_num1 [lemma, in Lcm_tes]
max_num2 [lemma, in Lcm_tes]
max_num_conm [lemma, in Lcm_tes]
monom [definition, in Monomes_tes]
Monomes_tes [library]
monom_op [definition, in Monomes_tes]
monot_no_zmonom [lemma, in Monomes_tes]
monot_suma [lemma, in Somme_poly_tes]
monot_suma_l [lemma, in Somme_poly_tes]
monot_suma_pol_mon [lemma, in nueva_equiv2_tes]
monot_zmonom [lemma, in Monomes_tes]
mon_coef [definition, in Monomes_tes]
mon_opp_term [lemma, in Monomes_tes]
mon_Q_cpol [lemma, in Somme_poly_tes]
mon_term [definition, in Monomes_tes]
mon_term_mult [lemma, in orden_term]
multQ [axiom, in Corps_tes]
multQ_assoc [axiom, in Corps_tes]
multQ_comp [lemma, in Corps_tes]
multQ_comp_l [lemma, in Corps_tes]
multQ_comp_r [axiom, in Corps_tes]
multQ_conm [axiom, in Corps_tes]
multQ_divQ1 [lemma, in Corps_tes]
multQ_neg [axiom, in Corps_tes]
multQ_neg1 [lemma, in Corps_tes]
multQ_neg2 [lemma, in Corps_tes]
multQ_neg_plusQ [lemma, in Corps_tes]
multQ_neg_unQ [lemma, in Corps_tes]
multQ_n_OQ [lemma, in Corps_tes]
multQ_n_z [lemma, in Corps_tes]
multQ_zero [lemma, in Corps_tes]
mult_div_term1 [lemma, in divisib_tes]
mult_m [definition, in Mult_poly_tes]
mult_mon [definition, in Monomes_tes]
mult_mon_asoc [lemma, in Monomes_tes]
mult_mon_comp_l [lemma, in Monomes_tes]
mult_mon_conm [lemma, in Monomes_tes]
mult_mon_perm [lemma, in Monomes_tes]
mult_m_asoc [lemma, in Mult_poly_tes]
mult_m_distr [lemma, in Mult_poly_tes]
mult_m_effic_cor_l [lemma, in prueba_tes]
mult_m_effic_full [lemma, in prueba_tes]
mult_m_effic_fun [definition, in prueba_tes]
mult_m_full [lemma, in prueba_tes]
mult_m_monom_opp [lemma, in Mult_poly_tes]
mult_m_vpol [lemma, in Mult_poly_tes]
mult_m_z_monom [lemma, in Mult_poly_tes]
mult_neg_unQ [lemma, in Mult_poly_tes]
mult_nz_monom [lemma, in Div_poly_tes]
mult_opp_monom2 [lemma, in Mult_poly_tes]
mult_p [definition, in Mult_poly_tes]
mult_pm_comp [lemma, in Mult_poly_tes]
mult_pm_comp_ss [lemma, in Mult_poly_tes]
mult_pm_comp_2 [lemma, in Mult_poly_tes]
Mult_poly_tes [library]
mult_p_assoc [lemma, in Mult_poly_tes]
mult_p_can [lemma, in prueba_tes]
mult_p_comp [lemma, in Mult_poly_tes]
mult_p_comp_r [lemma, in Mult_poly_tes]
mult_p_conm [lemma, in Mult_poly_tes]
mult_p_cpol [lemma, in Mult_poly_tes]
mult_p_effic_cor_l [lemma, in prueba_tes]
mult_p_effic_full [lemma, in prueba_tes]
mult_p_effic_fun [definition, in prueba_tes]
mult_p_id [lemma, in ideal_tes]
mult_p_m [lemma, in Mult_poly_tes]
mult_p_m_asoc [lemma, in Mult_poly_tes]
mult_Q_monom [definition, in Monomes_tes]
mult_Q_pol [definition, in Polynomes_tes]
mult_sum_opp1 [lemma, in ecuaciones_tes]
mult_sum_opp2 [lemma, in ecuaciones_tes]
mult_sum_opp3 [lemma, in Somme_poly_tes]
mult_vpol [lemma, in Mult_poly_tes]
mul_mon_full [lemma, in Monomes_tes]
mul_opp_monom [lemma, in Mult_poly_tes]

N

n [axiom, in Polynomes_tes]
nat_S_p [lemma, in Termes_tes]
neg_divQ [lemma, in Corps_tes]
neg_neg_Q [lemma, in Corps_tes]
neg_OQ [lemma, in Corps_tes]
neut_multQ [axiom, in Corps_tes]
neut_mult_m [lemma, in Mult_poly_tes]
neut_mult_p [lemma, in Mult_poly_tes]
neut_plusQ [axiom, in Corps_tes]
Newmansi [lemma, in ult_impl]
noetheriano [definition, in noetred_tes]
noether_Red1_full [definition, in ult_impl]
noeth_noether2 [lemma, in ult_impl]
noeth_noether2_inv [lemma, in ult_impl]
noetred_tes [library]
normal [definition, in normal_tes]
normal_eq [lemma, in normal_tes]
normal_eq_aux [lemma, in normal_tes]
normal_ext [lemma, in normal_tes]
normal_Red_normal [lemma, in normal_tes]
normal_tes [library]
norm_corr [lemma, in normal_tes]
no_divQ_zero [lemma, in Corps_tes]
no_div_term_fn [lemma, in normal_tes]
no_equpol_Ttm [lemma, in coeficiente_tes]
no_eq_no_vpol_opp [lemma, in Somme_poly_tes]
no_hterm_Ttm_in_red [lemma, in Hmtc_axiom]
no_hterm_Ttm_in_red_bis [lemma, in Hmtc_axiom]
no_mon_rep_full [lemma, in pol_can]
no_term_in_cpol [lemma, in coeficiente_tes]
no_term_in_pol [definition, in coeficiente_tes]
no_term_in_pol_opp [lemma, in coeficiente_tes]
no_trivial [axiom, in Corps_tes]
no_zero_invQ [lemma, in Corps_tes]
nterm_null [lemma, in Termes_tes]
nueva_equiv2_tes [library]
nuevo1 [lemma, in Corps_tes]
nuevo2 [lemma, in Corps_tes]
null_div [lemma, in divisib_tes]
null_term [inductive, in Termes_tes]
null_term_cons [constructor, in Termes_tes]
null_term_nil [constructor, in Termes_tes]
null_term_term_O [lemma, in Termes_tes]
nvpol_full_fam [lemma, in reduccion2_tes]
n_term_O [definition, in Termes_tes]
n_zmonom_n_vpol [lemma, in coeficiente_tes]

O

occ_n_vpol [lemma, in Hmtc]
oppm_idp [lemma, in ideal_tes]
opp_comp [lemma, in Somme_poly_tes]
opp_mult_m [lemma, in ecuaciones_tes]
opp_p_id [lemma, in ideal_tes]
opp_p_id2 [lemma, in ideal_tes]
opp_vpol [lemma, in Somme_poly_tes]
OQ [axiom, in Corps_tes]
orden_pol [library]
orden_term [library]
ord_adm1 [lemma, in orden_term]

P

permut_suma_app [lemma, in Somme_poly_tes]
plusQ [axiom, in Corps_tes]
plusQ_assoc [axiom, in Corps_tes]
plusQ_comp [lemma, in Corps_tes]
plusQ_comp_l [lemma, in Corps_tes]
plusQ_comp_r [axiom, in Corps_tes]
plusQ_conm [axiom, in Corps_tes]
plusQ_frac [lemma, in Corps_tes]
plusQ_zero [lemma, in Corps_tes]
plusQ_zero_nzero [lemma, in Corps_tes]
pol [inductive, in Polynomes_tes]
Polynomes_tes [library]
pol_can [library]
pol_eq_id_eg [lemma, in ideal_tes]
pol_fn_id [lemma, in normal_tes]
pol_fn_id2 [lemma, in normal_tes]
pol_full [definition, in orden_pol]
pol_F_idF [lemma, in ideal_tes]
pol_F_idmult [lemma, in ideal_tes]
pol_F_idmult_opp [lemma, in ideal_tes]
pol_f_impl_f_pol [lemma, in orden_pol]
pol_f_impl_f_term [lemma, in orden_pol]
pol_In_ensemb [inductive, in ideal_tes]
pol_In_ensemb_ext [lemma, in ideal_tes]
pol_In_ensemb_unic [lemma, in ideal_tes]
pol_In_hd [constructor, in ideal_tes]
pol_In_tl [constructor, in ideal_tes]
pol_Lex_rec [definition, in orden_pol]
pol_opp [definition, in Somme_poly_tes]
pol_opp_mult [lemma, in pol_can]
pol_recpol [definition, in orden_pol]
pol_rec_Tpol [lemma, in orden_pol]
pol_rec_Tpol_lex3 [lemma, in orden_pol]
prev_calcula_fn2 [lemma, in normal_tes]
prev_calcula_fn3bis [lemma, in normal_tes]
pre_basic4_Red1 [lemma, in red_expl]
pre_basic4_Red3 [lemma, in red_expl]
Prop_basic2_tes [library]
prueba_tes [library]
p_idp [lemma, in ideal_tes]

Q

Q [axiom, in Corps_tes]

R

red [inductive, in reduccion2_tes]
reduccion2_tes [library]
Red1 [inductive, in reduccion2_tes]
Red1_dif_id [lemma, in reduccion2_tes]
Red1_en_cons [lemma, in reduccion2_tes]
Red1_en_cons_inv [lemma, in reduccion2_tes]
Red1_en_id [lemma, in reduccion2_tes]
Red1_en_id_inv [lemma, in reduccion2_tes]
red1_exp_simpl [constructor, in reduccion2_tes]
Red1_ext1 [lemma, in reduccion2_tes]
Red1_ext2 [lemma, in reduccion2_tes]
Red1_is_common [lemma, in Axiomas_n_full2_tes]
Red1_menor2 [lemma, in noetred_tes]
Red1_mult_m [lemma, in reduccion2_tes]
Red1_simp [constructor, in reduccion2_tes]
red1_simpl [constructor, in reduccion2_tes]
Red1_vpol [lemma, in reduccion2_tes]
Red3 [inductive, in reduccion2_tes]
Red3_dif_id [lemma, in reduccion2_tes]
Red3_en_cons [lemma, in reduccion2_tes]
Red3_en_cons_inv [lemma, in reduccion2_tes]
Red3_en_id [lemma, in reduccion2_tes]
Red3_en_id_inv [lemma, in reduccion2_tes]
Red3_eq [constructor, in reduccion2_tes]
Red3_equiv [lemma, in congr_y_red2_tes]
Red3_ext1 [lemma, in reduccion2_tes]
Red3_ext2 [lemma, in reduccion2_tes]
red3_fFh [lemma, in reduccion2_tes]
red3_fFh2 [lemma, in reduccion2_tes]
red3_fFh_vpol [lemma, in reduccion2_tes]
Red3_full_fam [lemma, in reduccion2_tes]
Red3_full_l [lemma, in reduccion2_tes]
Red3_full_r [lemma, in reduccion2_tes]
Red3_mult_m [lemma, in reduccion2_tes]
Red3_norm [lemma, in normal_tes]
Red3_nuevo_Red1_bis_full [lemma, in ult_impl]
Red3_ste [lemma, in reduccion2_tes]
Red3_step [constructor, in reduccion2_tes]
Red3_tran [lemma, in reduccion2_tes]
Red3_trans [constructor, in reduccion2_tes]
Red3_vpol_mult_m [lemma, in reduccion2_tes]
Red3_vpol_normal [lemma, in normal_tes]
red_comp [lemma, in reduccion2_tes]
Red_equiv [inductive, in congr_y_red2_tes]
Red_equiv_eq [constructor, in congr_y_red2_tes]
Red_equiv_ext [lemma, in congr_y_red2_tes]
Red_equiv_full_l [lemma, in congr_y_red2_tes]
Red_equiv_full_r [lemma, in congr_y_red2_tes]
Red_equiv_step [constructor, in congr_y_red2_tes]
Red_equiv_sy [lemma, in congr_y_red2_tes]
Red_equiv_sym [constructor, in congr_y_red2_tes]
Red_equiv_tran [lemma, in congr_y_red2_tes]
Red_equiv_trans [constructor, in congr_y_red2_tes]
red_exp [inductive, in reduccion2_tes]
red_expl [library]
red_exp_impl_red [lemma, in reduccion2_tes]
red_ext1 [lemma, in reduccion2_tes]
red_ext2 [lemma, in reduccion2_tes]
red_ext3 [lemma, in reduccion2_tes]
red_f_f [lemma, in reduccion2_tes]
red_hred [lemma, in reduccion2_tes]
red_impl_red_exp [lemma, in reduccion2_tes]
red_menor2 [lemma, in noetred_tes]
red_n_vpol1 [lemma, in reduccion2_tes]
Red_vpol [lemma, in reduccion2_tes]
red_0_un_step [lemma, in reduccion2_tes]
regl_sig [lemma, in Mult_poly_tes]
resul_multQ_zero [lemma, in Corps_tes]

S

same_can [lemma, in pol_can]
same_cons [constructor, in pol_can]
same_equpol [lemma, in pol_can]
same_length [lemma, in pol_can]
same_nil [constructor, in pol_can]
same_pol [inductive, in pol_can]
same_refl [lemma, in pol_can]
same_sym [lemma, in pol_can]
same_trans [lemma, in pol_can]
simetrico [definition, in noetred_tes]
simpl_divQ [lemma, in Corps_tes]
simpl_term [lemma, in divisib_tes]
Somme_poly_tes [library]
split_mon_mon [lemma, in nueva_equiv2_tes]
split_pol [lemma, in coeficiente_tes]
split_pol_mon [lemma, in nueva_equiv2_tes]
split_term_in_pol [lemma, in coeficiente_tes]
split_term_in_pol_cons [lemma, in coeficiente_tes]
sufc_common [lemma, in Axiomas_n_full2_tes]
sufc_common1 [lemma, in Axiomas_n_full2_tes]
sufc_Red1 [lemma, in reduccion2_tes]
suma_app [definition, in Somme_poly_tes]
suma_app_full [lemma, in pol_can]
suma_cpol [lemma, in Somme_poly_tes]
suma_igual [lemma, in Corps_tes]
suma_op [lemma, in Corps_tes]
suma_opp [lemma, in Somme_poly_tes]
suma_op_inv [lemma, in Corps_tes]
suma_pol_mon [inductive, in nueva_equiv2_tes]
suma_pol_mon1 [constructor, in nueva_equiv2_tes]
suma_pol_mon2 [constructor, in nueva_equiv2_tes]
suma_p_id [lemma, in ideal_tes]
suma_vpol [lemma, in Somme_poly_tes]
suma_vpol_leibn [lemma, in Somme_poly_tes]
sumcpol_l [lemma, in Somme_poly_tes]
sum_vpol_opp [lemma, in Somme_poly_tes]
sum_vpol_opp_inv [lemma, in Somme_poly_tes]
sym_equiv_Id2 [lemma, in nueva_equiv2_tes]
sym_mon [lemma, in Somme_poly_tes]
sym_mon1 [lemma, in Somme_poly_tes]
S_imp_eq [lemma, in Termes_tes]
s_l_ord_pol [lemma, in orden_pol]
S_pol [definition, in S_poly_nuevo2_tes]
S_poly_nuevo2_tes [library]
S_pol_ext [lemma, in S_poly_nuevo2_tes]
S_pol_ff [lemma, in S_poly_nuevo2_tes]
S_pol_n_vpol [lemma, in S_poly_nuevo2_tes]
S_pol_sym [lemma, in S_poly_nuevo2_tes]
s_t_ord_p [lemma, in orden_pol]

T

term [definition, in Termes_tes]
Termes_tes [library]
term_div [inductive, in divisib_tes]
term_div_cons [constructor, in divisib_tes]
term_div_eq [lemma, in divisib_tes]
term_div_full [lemma, in divisib_tes]
term_div_full_nulo [lemma, in divisib_tes]
term_div_full_S [lemma, in divisib_tes]
term_div_hterm [lemma, in Hmtc]
term_div_null [constructor, in divisib_tes]
term_div_n_comp [lemma, in divisib_tes]
term_div_n_eq [lemma, in divisib_tes]
term_equpol [lemma, in coeficiente_tes]
term_equpol2 [lemma, in coeficiente_tes]
term_in_pol [definition, in coeficiente_tes]
term_in_pol_monom [lemma, in coeficiente_tes]
term_in_pol_nvpol [lemma, in coeficiente_tes]
term_in_pol_opp [lemma, in coeficiente_tes]
term_in_pol_same [lemma, in pol_can]
term_in_sum [lemma, in coeficiente_tes]
term_in_Ttm [lemma, in Hmtc]
term_in_Ttm_hterm [lemma, in Hmtc]
term_in_Ttm_pol [lemma, in pol_can]
term_monom_hterm [lemma, in Hmtc]
term_mult [definition, in Termes_tes]
term_mult_assoc [lemma, in Termes_tes]
term_mult_can_full [lemma, in Termes_tes]
term_mult_conmt [lemma, in Termes_tes]
term_mult_div [lemma, in divisib_tes]
term_mult_full [lemma, in Termes_tes]
term_mult_full_nulo [lemma, in Termes_tes]
term_mult_n_eq [lemma, in Termes_tes]
term_mult_perm [lemma, in Termes_tes]
term_mult_r [lemma, in Termes_tes]
Tpol_cpol_full [lemma, in orden_pol]
Tpol_full [definition, in orden_pol]
Tpol_full_wf [lemma, in orden_pol]
Tpol_Lex3 [inductive, in orden_pol]
Tpol_Lex3_car [constructor, in orden_pol]
Tpol_Lex3_cdr [constructor, in orden_pol]
Tpol_Lex3_no_refl [lemma, in orden_pol]
Tpol_Lex3_tran [lemma, in orden_pol]
Tpol_Lex3_v [constructor, in orden_pol]
Tpol_tran_mon [lemma, in orden_pol]
trans_common_red [lemma, in lemma_cong_red2_tes]
trans_common_red_full [lemma, in S_poly_nuevo2_tes]
trans_equiv_common [lemma, in lemma_cong_red2_tes]
trans_equiv_Id2 [lemma, in nueva_equiv2_tes]
Ttm [inductive, in orden_term]
Ttm_antisym [lemma, in orden_term]
Ttm_a2 [lemma, in orden_term]
Ttm_car [constructor, in orden_term]
Ttm_cdr [constructor, in orden_term]
Ttm_hterm [lemma, in Hmtc]
Ttm_nonrefl [lemma, in orden_term]
Ttm_no_term_in_pol [lemma, in coeficiente_tes]
Ttm_no_term_in_pol2 [lemma, in coeficiente_tes]
Ttm_pol_hterm [lemma, in Hmtc]
Ttm_shorter [lemma, in orden_term]
Ttm_strict [lemma, in orden_term]
Ttm_suma_hterm [lemma, in Hmtc]
Ttm_total [lemma, in orden_term]
Ttm_total_good [lemma, in orden_term]
Ttm_trans [lemma, in orden_term]
Ttm_wf [lemma, in orden_term]

U

ult_impl [library]
unQ [axiom, in Corps_tes]

V

vpol [constructor, in Polynomes_tes]
vpol_dec [lemma, in pol_can]
vpol_dec_full_term [lemma, in pol_can]
vpol_normal [lemma, in normal_tes]
vpol_suma [lemma, in Somme_poly_tes]
vpol_suma_leibn [lemma, in Somme_poly_tes]

Z

zero_multQ [lemma, in Corps_tes]
z_equmon [lemma, in Monomes_tes]
z_monom [definition, in Monomes_tes]
z_monom_dec [lemma, in Monomes_tes]

Axiom Index

D

decQ [in Corps_tes]
distrQ [in Corps_tes]

E

eqQ [in Corps_tes]
eqQ_refl [in Corps_tes]
eqQ_sym [in Corps_tes]
eqQ_trans [in Corps_tes]
ex_op [in Corps_tes]

I

invQ [in Corps_tes]
inv_divQ [in Corps_tes]

M

multQ [in Corps_tes]
multQ_assoc [in Corps_tes]
multQ_comp_r [in Corps_tes]
multQ_conm [in Corps_tes]
multQ_neg [in Corps_tes]

N

n [in Polynomes_tes]
neut_multQ [in Corps_tes]
neut_plusQ [in Corps_tes]
no_trivial [in Corps_tes]

O

OQ [in Corps_tes]

P

plusQ [in Corps_tes]
plusQ_assoc [in Corps_tes]
plusQ_comp_r [in Corps_tes]
plusQ_conm [in Corps_tes]

Q

Q [in Corps_tes]

U

unQ [in Corps_tes]

Lemma Index

A

add_effic [in prueba_tes]
add_effic_cor_l [in prueba_tes]
add_effic_full [in prueba_tes]
asoc_mon_pol [in Somme_poly_tes]
asoc_suma [in Somme_poly_tes]
auxiliar2 [in orden_pol]
aux1_hterm_eq_suma_Ttm [in Hmtc]
aux1_hterm_suma_Ttm [in Hmtc]
aux1_red_menor2 [in noetred_tes]
aux2_hterm_eq_suma_Ttm [in Hmtc]
aux2_red_menor2 [in noetred_tes]
aux_hterm_suma_Ttm [in Hmtc]
aux_no_hterm_Ttm_in_red [in Hmtc_axiom]
aux_suma_app_full [in pol_can]
ayuda_Benj [in ecuaciones_tes]
ayuda_full_imp_lis_desc [in orden_pol]
ayud_Gilb [in ecuaciones_tes]

B

basic2 [in red_expl]
basic2_bis [in red_expl]
basic3 [in red_expl]
basic3_full [in impl_large]
basic4 [in red_expl]
basic4_full [in impl_large]
buen_ord_red [in noetred_tes]
buen_ord_red1 [in noetred_tes]

C

calcula_fnbis [in normal_tes]
can_corr [in pol_can]
can_fun [in pol_can]
can_is_full [in pol_can]
caseRed1xy [in ult_impl]
ch_m_plus [in ecuaciones_tes]
ch_m_plus2 [in ecuaciones_tes]
coef_first [in pol_can]
coef_hterm [in Hmtc]
coef_low_pol [in pol_can]
coef_n_term [in coeficiente_tes]
coef_pol_opp [in coeficiente_tes]
coef_pol_opp2 [in coeficiente_tes]
coef_suma_pol [in coeficiente_tes]
coef_suma_Ttm [in Hmtc]
coef_term_mult [in coeficiente_tes]
coef_Ttm_split_pol [in coeficiente_tes]
coef_z_in_pol [in coeficiente_tes]
common_is_Red_equiv [in lemma_cong_red2_tes]
comm_mult_can [in pol_can]
comp_common_succ [in Axiomas_n_full2_tes]
comp_common_succ_full [in S_poly_nuevo2_tes]
comp_divis_lex [in divisib_tes]
comp_mult_m_effic [in prueba_tes]
comp_mult_p_effic [in prueba_tes]
comp_nOQ [in Corps_tes]
comp_no_term_in_pol [in coeficiente_tes]
comp_sum_effic [in prueba_tes]
comp_term_in_pol [in coeficiente_tes]
cond_ht_pol [in Hmtc]
congr_conv [in Axiomas_n_full2_tes]
conmt_common_succ [in lemma_cong_red2_tes]
conmt_common_succ_full [in S_poly_nuevo2_tes]
conmt_suma [in Somme_poly_tes]
cons_full_fam [in reduccion2_tes]
contr_hterm_vpol [in Hmtc]
contr_mult_nz_monom [in Div_poly_tes]
conv_congr [in congr_y_red2_tes]
con_red_cong [in congr_y_red2_tes]
cr_full [in S_poly_nuevo2_tes]

D

decQ_t [in Corps_tes]
dec_coef_monom [in Monomes_tes]
dec_sum_term_in_pol [in coeficiente_tes]
dec_term_div [in divisib_tes]
dec_term_in_pol [in coeficiente_tes]
Desc_rev [in orden_pol]
Desc_rev_pol [in orden_pol]
Diagrama [in ult_impl]
distr_divQ [in Corps_tes]
distr_div_suma [in Div_poly_tes]
distr_mult_m_monom [in Mult_poly_tes]
distr_mult_p [in Mult_poly_tes]
distr_mult_p_r [in Mult_poly_tes]
division [in Corps_tes]
divis_im_divt [in divisib_tes]
divQ_0 [in Corps_tes]
divQ_0_n [in Corps_tes]
div_lcm1 [in Lcm_tes]
div_lcm2 [in Lcm_tes]
div_mult_inv [in Div_poly_tes]
div_mult_mon_inv [in divisib_tes]
div_pm_comp [in Div_poly_tes]
div_Q_eq [in Corps_tes]
div_term_hterm [in Hmtc]
div_trans [in divisib_tes]

E

ec_invQ [in Corps_tes]
eg_denomQ [in Corps_tes]
eg_denom_term [in divisib_tes]
eg_numeraQ [in Corps_tes]
elem_full [in reduccion2_tes]
elem_n_vpol [in reduccion2_tes]
elim_red_exp [in reduccion2_tes]
eqexp_cons [in Termes_tes]
eqterm_cons1 [in Termes_tes]
equat1 [in ecuaciones_tes]
equat_equiv_Id [in nueva_equiv2_tes]
equiv_Id2_equiv_Id [in nueva_equiv2_tes]
equiv_Id_cpol [in nueva_equiv2_tes]
equiv_Id_equiv_Id2 [in nueva_equiv2_tes]
equiv_id_trans [in congr_y_red2_tes]
equiv_m [in nueva_equiv2_tes]
equmon_cons [in Somme_poly_tes]
equmon_refl [in Monomes_tes]
equmon_sym [in Monomes_tes]
equmon_trans [in Monomes_tes]
equmon_z [in Monomes_tes]
equm_full_hmonom [in Hmtc]
equm_refl [in Hmtc]
equm_sym [in Hmtc]
equm_trans [in Hmtc]
equpol_can [in Hmtc]
equpol_cpol [in Somme_poly_tes]
equpol_cpol2 [in Somme_poly_tes]
equpol_dec_full_term [in pol_can]
equpol_fn [in normal_tes]
equpol_Id_sum2 [in nueva_equiv2_tes]
equpol_Id_sum2_op [in nueva_equiv2_tes]
eq_coef_monom [in Hmtc]
eq_cpol [in Somme_poly_tes]
eq_hcoef [in Hmtc]
eq_homnom_fst [in Hmtc]
eq_hterm [in Hmtc]
eq_Ideal_eq_p [in ideal_tes]
eq_mon_cpol [in Somme_poly_tes]
eq_mulQ_neg [in Corps_tes]
eq_nvpol [in Somme_poly_tes]
eq_pol_opp_hcoef [in Hmtc]
eq_pol_opp_hterm [in Hmtc]
eq_pol_opp_no_zero [in Somme_poly_tes]
eq_Red_equiv_common [in Axiomas_n_full2_tes]
eq_term_div [in Hmtc]
eq_term_in_pol_monom [in coeficiente_tes]
eq_tm_dec [in Termes_tes]
ext_full_Tpol [in orden_pol]
ext_l_Tpol_Lex3 [in orden_pol]
ext_r_Tpol_Lex3 [in orden_pol]
ex_fpol [in orden_pol]
ex_fpol_eq [in orden_pol]
ex_term_div_n [in divisib_tes]

F

fn_equpol_vpol [in normal_tes]
fn_p_id [in normal_tes]
for_norm_dec_vpol [in normal_tes]
fst_equm [in Hmtc]
fst_mult [in Hmtc]
fullp_impl_fullt [in pol_can]
full_coef [in coeficiente_tes]
full_cp_neq_vp [in pol_can]
full_eq_vpol [in pol_can]
full_fam_dec [in reduccion2_tes]
full_hcoef [in Hmtc]
full_hterm [in Hmtc]
full_hterm_full_pol [in Hmtc]
full_imp_lis_desc [in orden_pol]
full_monom [in pol_can]
full_mult_m [in Mult_poly_tes]
full_mult_mon [in pol_can]
full_no_term [in pol_can]
full_O [in Termes_tes]
full_opp [in pol_can]
full_pol_cons_term [in pol_can]
full_pol_In_hterm [in reduccion2_tes]
full_pol_mon [in pol_can]
full_pol_tm_dec [in Polynomes_tes]
full_pred1 [in Termes_tes]
full_S [in Termes_tes]
full_same [in pol_can]
full_term_cpol [in Polynomes_tes]
full_term_full_fam [in reduccion2_tes]
full_term_mult_p [in Mult_poly_tes]
full_term_norm [in normal_tes]
full_term_opp [in Somme_poly_tes]
full_term_pol_mon [in Polynomes_tes]
full_term_suma_app [in Somme_poly_tes]
full_term_S_pol [in S_poly_nuevo2_tes]
full_tm_dec [in Polynomes_tes]
full_Ttm_pol_hterm [in Hmtc]
funcanvpol [in Hmtc]

G

gen_split_pol [in coeficiente_tes]
gr_ht_nvpol [in Hmtc]
G1_impl_G2_full [in S_poly_nuevo2_tes]
G2_impl_G1_full [in ult_impl]
G2_impl_G3_LCR_full [in impl_large]
G3CR_L_impl_G3CR_full [in ult_impl]
G3_CR_impl_G1_full [in S_poly_nuevo2_tes]
G3_CR_impl_G3_full [in S_poly_nuevo2_tes]

H

hcoef_mult [in Hmtc]
hcoef_mult2 [in Hmtc]
hcoef_no_eq_hterm [in Hmtc]
hcoef_pol_opp [in Hmtc]
hcoef_pol_opp_term [in Hmtc]
hcoef_suma_Ttm [in Hmtc]
hcoef_vpol [in Hmtc]
hmct_Leib [in Hmtc]
hmonom_mult [in Hmtc]
hred_suma [in red_expl]
hred_suma_bis [in red_expl]
hterm_eq_suma_Ttm [in Hmtc]
hterm_mult_m [in Hmtc]
hterm_mult_m2 [in Hmtc]
hterm_pol_m_opp [in Hmtc]
hterm_pol_opp [in Hmtc]
hterm_pol_opp_term [in Hmtc]
hterm_suma_Ttm [in Hmtc]
hterm_vpol [in Hmtc]

I

ideal_mon [in ideal_tes]
ideal_suma_pol_mon [in nueva_equiv2_tes]
id_trans [in ideal_tes]
igual [in Corps_tes]
imp_equiv_Id2_opp [in nueva_equiv2_tes]
Ind_prueba [in ult_impl]
insert [in pol_can]

L

lcm_conm [in Lcm_tes]
lcm_div [in Lcm_tes]
lcm_div2 [in Lcm_tes]
lcm_full [in Lcm_tes]
lcm_1 [in Lcm_tes]
lcm_2 [in Lcm_tes]
length_n_term_O [in Termes_tes]
list_indlg [in orden_term]
low_opp [in pol_can]
low_pol_cpol [in pol_can]
low_pol_term_mult [in pol_can]
low_trans [in pol_can]
Low_Ttm_tran [in pol_can]

M

max_numO [in Lcm_tes]
max_num1 [in Lcm_tes]
max_num2 [in Lcm_tes]
max_num_conm [in Lcm_tes]
monot_no_zmonom [in Monomes_tes]
monot_suma [in Somme_poly_tes]
monot_suma_l [in Somme_poly_tes]
monot_suma_pol_mon [in nueva_equiv2_tes]
monot_zmonom [in Monomes_tes]
mon_opp_term [in Monomes_tes]
mon_Q_cpol [in Somme_poly_tes]
mon_term_mult [in orden_term]
multQ_comp [in Corps_tes]
multQ_comp_l [in Corps_tes]
multQ_divQ1 [in Corps_tes]
multQ_neg1 [in Corps_tes]
multQ_neg2 [in Corps_tes]
multQ_neg_plusQ [in Corps_tes]
multQ_neg_unQ [in Corps_tes]
multQ_n_OQ [in Corps_tes]
multQ_n_z [in Corps_tes]
multQ_zero [in Corps_tes]
mult_div_term1 [in divisib_tes]
mult_mon_asoc [in Monomes_tes]
mult_mon_comp_l [in Monomes_tes]
mult_mon_conm [in Monomes_tes]
mult_mon_perm [in Monomes_tes]
mult_m_asoc [in Mult_poly_tes]
mult_m_distr [in Mult_poly_tes]
mult_m_effic_cor_l [in prueba_tes]
mult_m_effic_full [in prueba_tes]
mult_m_full [in prueba_tes]
mult_m_monom_opp [in Mult_poly_tes]
mult_m_vpol [in Mult_poly_tes]
mult_m_z_monom [in Mult_poly_tes]
mult_neg_unQ [in Mult_poly_tes]
mult_nz_monom [in Div_poly_tes]
mult_opp_monom2 [in Mult_poly_tes]
mult_pm_comp [in Mult_poly_tes]
mult_pm_comp_ss [in Mult_poly_tes]
mult_pm_comp_2 [in Mult_poly_tes]
mult_p_assoc [in Mult_poly_tes]
mult_p_can [in prueba_tes]
mult_p_comp [in Mult_poly_tes]
mult_p_comp_r [in Mult_poly_tes]
mult_p_conm [in Mult_poly_tes]
mult_p_cpol [in Mult_poly_tes]
mult_p_effic_cor_l [in prueba_tes]
mult_p_effic_full [in prueba_tes]
mult_p_id [in ideal_tes]
mult_p_m [in Mult_poly_tes]
mult_p_m_asoc [in Mult_poly_tes]
mult_sum_opp1 [in ecuaciones_tes]
mult_sum_opp2 [in ecuaciones_tes]
mult_sum_opp3 [in Somme_poly_tes]
mult_vpol [in Mult_poly_tes]
mul_mon_full [in Monomes_tes]
mul_opp_monom [in Mult_poly_tes]

N

nat_S_p [in Termes_tes]
neg_divQ [in Corps_tes]
neg_neg_Q [in Corps_tes]
neg_OQ [in Corps_tes]
neut_mult_m [in Mult_poly_tes]
neut_mult_p [in Mult_poly_tes]
Newmansi [in ult_impl]
noeth_noether2 [in ult_impl]
noeth_noether2_inv [in ult_impl]
normal_eq [in normal_tes]
normal_eq_aux [in normal_tes]
normal_ext [in normal_tes]
normal_Red_normal [in normal_tes]
norm_corr [in normal_tes]
no_divQ_zero [in Corps_tes]
no_div_term_fn [in normal_tes]
no_equpol_Ttm [in coeficiente_tes]
no_eq_no_vpol_opp [in Somme_poly_tes]
no_hterm_Ttm_in_red [in Hmtc_axiom]
no_hterm_Ttm_in_red_bis [in Hmtc_axiom]
no_mon_rep_full [in pol_can]
no_term_in_cpol [in coeficiente_tes]
no_term_in_pol_opp [in coeficiente_tes]
no_zero_invQ [in Corps_tes]
nterm_null [in Termes_tes]
nuevo1 [in Corps_tes]
nuevo2 [in Corps_tes]
null_div [in divisib_tes]
null_term_term_O [in Termes_tes]
nvpol_full_fam [in reduccion2_tes]
n_zmonom_n_vpol [in coeficiente_tes]

O

occ_n_vpol [in Hmtc]
oppm_idp [in ideal_tes]
opp_comp [in Somme_poly_tes]
opp_mult_m [in ecuaciones_tes]
opp_p_id [in ideal_tes]
opp_p_id2 [in ideal_tes]
opp_vpol [in Somme_poly_tes]
ord_adm1 [in orden_term]

P

permut_suma_app [in Somme_poly_tes]
plusQ_comp [in Corps_tes]
plusQ_comp_l [in Corps_tes]
plusQ_frac [in Corps_tes]
plusQ_zero [in Corps_tes]
plusQ_zero_nzero [in Corps_tes]
pol_eq_id_eg [in ideal_tes]
pol_fn_id [in normal_tes]
pol_fn_id2 [in normal_tes]
pol_F_idF [in ideal_tes]
pol_F_idmult [in ideal_tes]
pol_F_idmult_opp [in ideal_tes]
pol_f_impl_f_pol [in orden_pol]
pol_f_impl_f_term [in orden_pol]
pol_In_ensemb_ext [in ideal_tes]
pol_In_ensemb_unic [in ideal_tes]
pol_opp_mult [in pol_can]
pol_rec_Tpol [in orden_pol]
pol_rec_Tpol_lex3 [in orden_pol]
prev_calcula_fn2 [in normal_tes]
prev_calcula_fn3bis [in normal_tes]
pre_basic4_Red1 [in red_expl]
pre_basic4_Red3 [in red_expl]
p_idp [in ideal_tes]

R

Red1_dif_id [in reduccion2_tes]
Red1_en_cons [in reduccion2_tes]
Red1_en_cons_inv [in reduccion2_tes]
Red1_en_id [in reduccion2_tes]
Red1_en_id_inv [in reduccion2_tes]
Red1_ext1 [in reduccion2_tes]
Red1_ext2 [in reduccion2_tes]
Red1_is_common [in Axiomas_n_full2_tes]
Red1_menor2 [in noetred_tes]
Red1_mult_m [in reduccion2_tes]
Red1_vpol [in reduccion2_tes]
Red3_dif_id [in reduccion2_tes]
Red3_en_cons [in reduccion2_tes]
Red3_en_cons_inv [in reduccion2_tes]
Red3_en_id [in reduccion2_tes]
Red3_en_id_inv [in reduccion2_tes]
Red3_equiv [in congr_y_red2_tes]
Red3_ext1 [in reduccion2_tes]
Red3_ext2 [in reduccion2_tes]
red3_fFh [in reduccion2_tes]
red3_fFh2 [in reduccion2_tes]
red3_fFh_vpol [in reduccion2_tes]
Red3_full_fam [in reduccion2_tes]
Red3_full_l [in reduccion2_tes]
Red3_full_r [in reduccion2_tes]
Red3_mult_m [in reduccion2_tes]
Red3_norm [in normal_tes]
Red3_nuevo_Red1_bis_full [in ult_impl]
Red3_ste [in reduccion2_tes]
Red3_tran [in reduccion2_tes]
Red3_vpol_mult_m [in reduccion2_tes]
Red3_vpol_normal [in normal_tes]
red_comp [in reduccion2_tes]
Red_equiv_ext [in congr_y_red2_tes]
Red_equiv_full_l [in congr_y_red2_tes]
Red_equiv_full_r [in congr_y_red2_tes]
Red_equiv_sy [in congr_y_red2_tes]
Red_equiv_tran [in congr_y_red2_tes]
red_exp_impl_red [in reduccion2_tes]
red_ext1 [in reduccion2_tes]
red_ext2 [in reduccion2_tes]
red_ext3 [in reduccion2_tes]
red_f_f [in reduccion2_tes]
red_hred [in reduccion2_tes]
red_impl_red_exp [in reduccion2_tes]
red_menor2 [in noetred_tes]
red_n_vpol1 [in reduccion2_tes]
Red_vpol [in reduccion2_tes]
red_0_un_step [in reduccion2_tes]
regl_sig [in Mult_poly_tes]
resul_multQ_zero [in Corps_tes]

S

same_can [in pol_can]
same_equpol [in pol_can]
same_length [in pol_can]
same_refl [in pol_can]
same_sym [in pol_can]
same_trans [in pol_can]
simpl_divQ [in Corps_tes]
simpl_term [in divisib_tes]
split_mon_mon [in nueva_equiv2_tes]
split_pol [in coeficiente_tes]
split_pol_mon [in nueva_equiv2_tes]
split_term_in_pol [in coeficiente_tes]
split_term_in_pol_cons [in coeficiente_tes]
sufc_common [in Axiomas_n_full2_tes]
sufc_common1 [in Axiomas_n_full2_tes]
sufc_Red1 [in reduccion2_tes]
suma_app_full [in pol_can]
suma_cpol [in Somme_poly_tes]
suma_igual [in Corps_tes]
suma_op [in Corps_tes]
suma_opp [in Somme_poly_tes]
suma_op_inv [in Corps_tes]
suma_p_id [in ideal_tes]
suma_vpol [in Somme_poly_tes]
suma_vpol_leibn [in Somme_poly_tes]
sumcpol_l [in Somme_poly_tes]
sum_vpol_opp [in Somme_poly_tes]
sum_vpol_opp_inv [in Somme_poly_tes]
sym_equiv_Id2 [in nueva_equiv2_tes]
sym_mon [in Somme_poly_tes]
sym_mon1 [in Somme_poly_tes]
S_imp_eq [in Termes_tes]
s_l_ord_pol [in orden_pol]
S_pol_ext [in S_poly_nuevo2_tes]
S_pol_ff [in S_poly_nuevo2_tes]
S_pol_n_vpol [in S_poly_nuevo2_tes]
S_pol_sym [in S_poly_nuevo2_tes]
s_t_ord_p [in orden_pol]

T

term_div_eq [in divisib_tes]
term_div_full [in divisib_tes]
term_div_full_nulo [in divisib_tes]
term_div_full_S [in divisib_tes]
term_div_hterm [in Hmtc]
term_div_n_comp [in divisib_tes]
term_div_n_eq [in divisib_tes]
term_equpol [in coeficiente_tes]
term_equpol2 [in coeficiente_tes]
term_in_pol_monom [in coeficiente_tes]
term_in_pol_nvpol [in coeficiente_tes]
term_in_pol_opp [in coeficiente_tes]
term_in_pol_same [in pol_can]
term_in_sum [in coeficiente_tes]
term_in_Ttm [in Hmtc]
term_in_Ttm_hterm [in Hmtc]
term_in_Ttm_pol [in pol_can]
term_monom_hterm [in Hmtc]
term_mult_assoc [in Termes_tes]
term_mult_can_full [in Termes_tes]
term_mult_conmt [in Termes_tes]
term_mult_div [in divisib_tes]
term_mult_full [in Termes_tes]
term_mult_full_nulo [in Termes_tes]
term_mult_n_eq [in Termes_tes]
term_mult_perm [in Termes_tes]
term_mult_r [in Termes_tes]
Tpol_cpol_full [in orden_pol]
Tpol_full_wf [in orden_pol]
Tpol_Lex3_no_refl [in orden_pol]
Tpol_Lex3_tran [in orden_pol]
Tpol_tran_mon [in orden_pol]
trans_common_red [in lemma_cong_red2_tes]
trans_common_red_full [in S_poly_nuevo2_tes]
trans_equiv_common [in lemma_cong_red2_tes]
trans_equiv_Id2 [in nueva_equiv2_tes]
Ttm_antisym [in orden_term]
Ttm_a2 [in orden_term]
Ttm_hterm [in Hmtc]
Ttm_nonrefl [in orden_term]
Ttm_no_term_in_pol [in coeficiente_tes]
Ttm_no_term_in_pol2 [in coeficiente_tes]
Ttm_pol_hterm [in Hmtc]
Ttm_shorter [in orden_term]
Ttm_strict [in orden_term]
Ttm_suma_hterm [in Hmtc]
Ttm_total [in orden_term]
Ttm_total_good [in orden_term]
Ttm_trans [in orden_term]
Ttm_wf [in orden_term]

V

vpol_dec [in pol_can]
vpol_dec_full_term [in pol_can]
vpol_normal [in normal_tes]
vpol_suma [in Somme_poly_tes]
vpol_suma_leibn [in Somme_poly_tes]

Z

zero_multQ [in Corps_tes]
z_equmon [in Monomes_tes]
z_monom_dec [in Monomes_tes]

Constructor Index

C

common_succ_red [in lemma_cong_red2_tes]
common_succ_red_full [in S_poly_nuevo2_tes]
common_succ_step_red [in lemma_cong_red2_tes]
cpol [in Polynomes_tes]

E

equiv_Id_cons [in congr_y_red2_tes]
equmoni [in Hmtc]
equpol_cm [in Somme_poly_tes]
equpol_elim [in Somme_poly_tes]
equpol_refl [in Somme_poly_tes]
equpol_smt [in Somme_poly_tes]
equpol_ss [in Somme_poly_tes]
equpol_sym [in Somme_poly_tes]
equpol_tran [in Somme_poly_tes]

F

For_all_cs [in reduccion2_tes]
For_all_nil [in reduccion2_tes]
full_pol_cons [in pol_can]
full_pol_nil [in pol_can]
full_term_pol_cons [in Polynomes_tes]
full_term_pol_nil [in Polynomes_tes]

H

hred1_simpl [in reduccion2_tes]

I

ideal_cpol [in ideal_tes]
ideal_vpol [in ideal_tes]

L

low_cons [in pol_can]
low_nil [in pol_can]

N

null_term_cons [in Termes_tes]
null_term_nil [in Termes_tes]

P

pol_In_hd [in ideal_tes]
pol_In_tl [in ideal_tes]

R

red1_exp_simpl [in reduccion2_tes]
Red1_simp [in reduccion2_tes]
red1_simpl [in reduccion2_tes]
Red3_eq [in reduccion2_tes]
Red3_step [in reduccion2_tes]
Red3_trans [in reduccion2_tes]
Red_equiv_eq [in congr_y_red2_tes]
Red_equiv_step [in congr_y_red2_tes]
Red_equiv_sym [in congr_y_red2_tes]
Red_equiv_trans [in congr_y_red2_tes]

S

same_cons [in pol_can]
same_nil [in pol_can]
suma_pol_mon1 [in nueva_equiv2_tes]
suma_pol_mon2 [in nueva_equiv2_tes]

T

term_div_cons [in divisib_tes]
term_div_null [in divisib_tes]
Tpol_Lex3_car [in orden_pol]
Tpol_Lex3_cdr [in orden_pol]
Tpol_Lex3_v [in orden_pol]
Ttm_car [in orden_term]
Ttm_cdr [in orden_term]

V

vpol [in Polynomes_tes]

Inductive Index

C

common_succ [in lemma_cong_red2_tes]
common_succ_full [in S_poly_nuevo2_tes]
common_succ_step [in lemma_cong_red2_tes]

E

equiv_Id [in congr_y_red2_tes]
equm [in Hmtc]
equpol [in Somme_poly_tes]

F

for_all_list_pol [in reduccion2_tes]
full_pol [in pol_can]
full_term_pol [in Polynomes_tes]

H

hred [in reduccion2_tes]

I

Ideal [in ideal_tes]

L

low_pol [in pol_can]

N

null_term [in Termes_tes]

P

pol [in Polynomes_tes]
pol_In_ensemb [in ideal_tes]

R

red [in reduccion2_tes]
Red1 [in reduccion2_tes]
Red3 [in reduccion2_tes]
Red_equiv [in congr_y_red2_tes]
red_exp [in reduccion2_tes]

S

same_pol [in pol_can]
suma_pol_mon [in nueva_equiv2_tes]

T

term_div [in divisib_tes]
Tpol_Lex3 [in orden_pol]
Ttm [in orden_term]

Definition Index

A

add_effic_fun [in prueba_tes]

C

coef [in coeficiente_tes]
confluente [in S_poly_nuevo2_tes]
confluente_full [in S_poly_nuevo2_tes]

D

divQ [in Corps_tes]
div_m [in Div_poly_tes]
div_mon [in Monomes_tes]
div_term [in divisib_tes]

E

equmon [in Monomes_tes]
eq_Ideal [in ideal_tes]

F

for_norm [in normal_tes]
fst_term [in Hmtc]
full [in Termes_tes]
full_fam [in reduccion2_tes]
full_mon [in Monomes_tes]
fun_can [in pol_can]

G

Groebner1_full [in S_poly_nuevo2_tes]
Groebner2_full [in S_poly_nuevo2_tes]
Groebner3_CR_full [in S_poly_nuevo2_tes]
Groebner3_full [in S_poly_nuevo2_tes]

H

hcoef [in Hmtc]
hmonom [in Hmtc]
hterm [in Hmtc]

I

Ideal_ens [in ideal_tes]
inc [in orden_pol]
inc_list [in orden_pol]
inc_red [in noetred_tes]
inc_Red1 [in noetred_tes]

L

lcm [in Lcm_tes]
Listterm_desc [in orden_pol]
local_confluente_full [in ult_impl]

M

max_num [in Lcm_tes]
monom [in Monomes_tes]
monom_op [in Monomes_tes]
mon_coef [in Monomes_tes]
mon_term [in Monomes_tes]
mult_m [in Mult_poly_tes]
mult_mon [in Monomes_tes]
mult_m_effic_fun [in prueba_tes]
mult_p [in Mult_poly_tes]
mult_p_effic_fun [in prueba_tes]
mult_Q_monom [in Monomes_tes]
mult_Q_pol [in Polynomes_tes]

N

noetheriano [in noetred_tes]
noether_Red1_full [in ult_impl]
normal [in normal_tes]
no_term_in_pol [in coeficiente_tes]
n_term_O [in Termes_tes]

P

pol_full [in orden_pol]
pol_Lex_rec [in orden_pol]
pol_opp [in Somme_poly_tes]
pol_recpol [in orden_pol]

S

simetrico [in noetred_tes]
suma_app [in Somme_poly_tes]
S_pol [in S_poly_nuevo2_tes]

T

term [in Termes_tes]
term_in_pol [in coeficiente_tes]
term_mult [in Termes_tes]
Tpol_full [in orden_pol]

Z

z_monom [in Monomes_tes]

Library Index

A

Axiomas_n_full2_tes

C

coeficiente_tes
congr_y_red2_tes
Corps_tes

D

divisib_tes
Div_poly_tes

E

H

Hmtc
Hmtc_axiom

I

ideal_tes
impl_large

L

Lcm_tes
lemma_cong_red2_tes

M

Monomes_tes
Mult_poly_tes

N

noetred_tes
normal_tes
nueva_equiv2_tes

O

orden_pol
orden_term

P

Polynomes_tes
pol_can
Prop_basic2_tes
prueba_tes

R

reduccion2_tes
red_expl

S

Somme_poly_tes
S_poly_nuevo2_tes

T

U

Global Index

J

K

W

X

Y

_

(687 entries)

Axiom Index

A

B

C

F

G

H

J

K

L

R

S

T

V

W

X

Y

Z

_

(25 entries)

Lemma Index

J

K

Q

U

W

X

Y

_

(497 entries)

Constructor Index

A

B

D

G

J

K

M

O

Q

U

W

X

Y

Z

_

(50 entries)

Inductive Index

A

B

D

G

J

K

M

O

Q

U

V

W

X

Y

Z

_

(25 entries)

Definition Index

B

J

K

O

Q

R

U

V

W

X

Y

_

(60 entries)

Library Index

B

F

G

J

K

Q

V

W

X

Y

Z

_

(30 entries)

This page has been generated by coqdoc