X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCPoly_Degree.ma;h=35b49ac2c7b5abcabdc72590b07dc685b26c33e6;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=a7551f2f7372e9e1aaa885c482892eddde98cdb3;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma index a7551f2f7..35b49ac2c 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma @@ -16,15 +16,13 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_Degree". +include "CoRN.ma". + (* $Id: CPoly_Degree.v,v 1.5 2004/04/23 10:00:53 lcf Exp $ *) -(* INCLUDE -CPoly_NthCoeff -*) +include "algebra/CPoly_NthCoeff.ma". -(* INCLUDE -CFields -*) +include "algebra/CFields.ma". (*#* *Degrees of Polynomials ** Degrees of polynomials over a ring @@ -38,7 +36,7 @@ over [R]. Section Degree_def. *) -inline cic:/CoRN/algebra/CPoly_Degree/R.var. +inline "cic:/CoRN/algebra/CPoly_Degree/R.var". (* begin hide *) @@ -53,7 +51,7 @@ is always [1] higher than the `degree' (assuming that the highest coefficient is [[#]Zero])! *) -inline cic:/CoRN/algebra/CPoly_Degree/lth_of_poly.con. +inline "cic:/CoRN/algebra/CPoly_Degree/lth_of_poly.con". (*#* When dealing with constructive polynomials, notably over the reals or @@ -70,17 +68,17 @@ X^(n-1)#, if $p_i \mathrel{\#}0$#pi apart from 0#, we can say that the that the `degree is at most [j]'. *) -inline cic:/CoRN/algebra/CPoly_Degree/degree_le.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic.con". -inline cic:/CoRN/algebra/CPoly_Degree/odd_cpoly.con. +inline "cic:/CoRN/algebra/CPoly_Degree/odd_cpoly.con". -inline cic:/CoRN/algebra/CPoly_Degree/even_cpoly.con. +inline "cic:/CoRN/algebra/CPoly_Degree/even_cpoly.con". -inline cic:/CoRN/algebra/CPoly_Degree/regular.con. +inline "cic:/CoRN/algebra/CPoly_Degree/regular.con". (* UNEXPORTED End Degree_def. @@ -106,93 +104,93 @@ Implicit Arguments lth_of_poly [R]. Section Degree_props. *) -inline cic:/CoRN/algebra/CPoly_Degree/R.var. +inline "cic:/CoRN/algebra/CPoly_Degree/R.var". (* begin hide *) (* end hide *) -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_wd.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_wd.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_wd.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_wd.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic_wd.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_wd.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_imp_degree_le.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_imp_degree_le.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_c_.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_c_.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_c_.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_c_.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic_c_one.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_c_one.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_x_.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_x_.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_x_.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_x_.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic_x_.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_x_.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_mon.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_mon.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_inv.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_inv.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_plus.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_plus.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_minus.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_minus.con". -inline cic:/CoRN/algebra/CPoly_Degree/Sum_degree_le.con. +inline "cic:/CoRN/algebra/CPoly_Degree/Sum_degree_le.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_inv.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_inv.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_plus_rht.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_plus_rht.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_minus_lft.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_minus_lft.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic_plus.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_plus.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic_minus.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_minus.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_mult.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_mult.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_mult_aux.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_mult_aux.con". (* UNEXPORTED Hint Resolve degree_mult_aux: algebra. *) -inline cic:/CoRN/algebra/CPoly_Degree/monic_mult.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_mult.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_nexp.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_nexp.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic_nexp.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_nexp.con". -inline cic:/CoRN/algebra/CPoly_Degree/lt_i_lth_of_poly.con. +inline "cic:/CoRN/algebra/CPoly_Degree/lt_i_lth_of_poly.con". -inline cic:/CoRN/algebra/CPoly_Degree/poly_degree_lth.con. +inline "cic:/CoRN/algebra/CPoly_Degree/poly_degree_lth.con". -inline cic:/CoRN/algebra/CPoly_Degree/Cpoly_ex_degree.con. +inline "cic:/CoRN/algebra/CPoly_Degree/Cpoly_ex_degree.con". -inline cic:/CoRN/algebra/CPoly_Degree/poly_as_sum''.con. +inline "cic:/CoRN/algebra/CPoly_Degree/poly_as_sum''.con". (* UNEXPORTED Hint Resolve poly_as_sum'': algebra. *) -inline cic:/CoRN/algebra/CPoly_Degree/poly_as_sum'.con. +inline "cic:/CoRN/algebra/CPoly_Degree/poly_as_sum'.con". -inline cic:/CoRN/algebra/CPoly_Degree/poly_as_sum.con. +inline "cic:/CoRN/algebra/CPoly_Degree/poly_as_sum.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_zero.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_zero.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_1_imp.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_1_imp.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_cpoly_linear.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_cpoly_linear.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic_cpoly_linear.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_cpoly_linear.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic_one.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_one.con". -inline cic:/CoRN/algebra/CPoly_Degree/monic_apzero.con. +inline "cic:/CoRN/algebra/CPoly_Degree/monic_apzero.con". (* UNEXPORTED End Degree_props. @@ -216,19 +214,19 @@ polynomials over [F]. %\end{convention}% *) -inline cic:/CoRN/algebra/CPoly_Degree/F.var. +inline "cic:/CoRN/algebra/CPoly_Degree/F.var". (* begin hide *) (* end hide *) -inline cic:/CoRN/algebra/CPoly_Degree/degree_mult.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_mult.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_nexp.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_nexp.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_le_mult_imp.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_mult_imp.con". -inline cic:/CoRN/algebra/CPoly_Degree/degree_mult_imp.con. +inline "cic:/CoRN/algebra/CPoly_Degree/degree_mult_imp.con". (* UNEXPORTED End degree_props_Field.