X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCPoly_Degree.ma;h=79ec88e17a1b4b6601ec283e6a853f19eb29028e;hb=0a9ed4329c069d2e06902934b6d1d58d3690959c;hp=a7551f2f7372e9e1aaa885c482892eddde98cdb3;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma b/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma index a7551f2f7..79ec88e17 100644 --- a/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma +++ b/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 @@ -35,13 +33,17 @@ over [R]. *) (* UNEXPORTED -Section Degree_def. +Section Degree_def *) -inline cic:/CoRN/algebra/CPoly_Degree/R.var. +alias id "R" = "cic:/CoRN/algebra/CPoly_Degree/Degree_def/R.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) (*#* @@ -53,7 +55,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,20 +72,20 @@ 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. +End Degree_def *) (* UNEXPORTED @@ -103,99 +105,103 @@ Implicit Arguments lth_of_poly [R]. *) (* UNEXPORTED -Section Degree_props. +Section Degree_props *) -inline cic:/CoRN/algebra/CPoly_Degree/R.var. +alias id "R" = "cic:/CoRN/algebra/CPoly_Degree/Degree_props/R.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* 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. +End Degree_props *) (* UNEXPORTED @@ -207,7 +213,7 @@ Hint Resolve degree_mult_aux: algebra. *) (* UNEXPORTED -Section degree_props_Field. +Section degree_props_Field *) (*#* ** Degrees of polynomials over a field @@ -216,21 +222,25 @@ polynomials over [F]. %\end{convention}% *) -inline cic:/CoRN/algebra/CPoly_Degree/F.var. +alias id "F" = "cic:/CoRN/algebra/CPoly_Degree/degree_props_Field/F.var". (* begin hide *) +(* NOTATION +Notation FX := (cpoly_cring F). +*) + (* 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. +End degree_props_Field *)