X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCPoly_ApZero.ma;h=9a72ec02a9e6c4768d9541958a9578ea1c42df07;hb=f2d9db85559c7a8db11aae1153495fae4a258d54;hp=d6839ae4043087122bfa3385adcc9758f945ba1c;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma index d6839ae40..9a72ec02a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma @@ -16,26 +16,24 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_ApZero". +include "CoRN.ma". + (* $Id: CPoly_ApZero.v,v 1.3 2004/04/23 10:00:53 lcf Exp $ *) -(* INCLUDE -CPoly_Degree -*) +include "algebra/CPoly_Degree.ma". -(* INCLUDE -COrdFields2 -*) +include "algebra/COrdFields2.ma". (*#* * Polynomials apart from zero *) -inline cic:/CoRN/algebra/CPoly_ApZero/distinct1.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/distinct1.con". (* UNEXPORTED Implicit Arguments distinct1 [A]. *) (* UNEXPORTED -Section Poly_Representation. +Section Poly_Representation *) (*#* @@ -47,94 +45,94 @@ has degree at most [n]. %\end{convention}% *) -inline cic:/CoRN/algebra/CPoly_ApZero/R.var. +alias id "R" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/R.var". -inline cic:/CoRN/algebra/CPoly_ApZero/a_.var. +alias id "a_" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/a_.var". -inline cic:/CoRN/algebra/CPoly_ApZero/distinct_a_.var. +alias id "distinct_a_" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/distinct_a_.var". -inline cic:/CoRN/algebra/CPoly_ApZero/f.var. +alias id "f" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/f.var". -inline cic:/CoRN/algebra/CPoly_ApZero/n.var. +alias id "n" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/n.var". -inline cic:/CoRN/algebra/CPoly_ApZero/degree_f.var. +alias id "degree_f" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/degree_f.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) -(* INCLUDE -Transparent_algebra -*) +include "tactics/Transparent_algebra.ma". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_linear_shifted.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_linear_shifted.con". -(* INCLUDE -Opaque_algebra -*) +include "tactics/Opaque_algebra.ma". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_linear_factor.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_linear_factor.con". -inline cic:/CoRN/algebra/CPoly_ApZero/zero_poly.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/zero_poly.con". -inline cic:/CoRN/algebra/CPoly_ApZero/identical_poly.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/identical_poly.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_degree.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_degree.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_zero.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_zero.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_apzero.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_apzero.con". (* UNEXPORTED Hint Resolve poly_01_factor'_zero. *) -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_degree.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_degree.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_zero.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_zero.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_one.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_one.con". (* UNEXPORTED Hint Resolve poly_01_factor_zero poly_01_factor_one: algebra. *) -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree'.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree'.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_zero.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_zero.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_one.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_01_one.con". (* UNEXPORTED Hint Resolve poly_01_zero poly_01_one: algebra. *) -inline cic:/CoRN/algebra/CPoly_ApZero/poly_representation''.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_representation''.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_representation'.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_representation'.con". -inline cic:/CoRN/algebra/CPoly_ApZero/poly_representation.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_representation.con". (* UNEXPORTED Hint Resolve poly_representation: algebra. *) -inline cic:/CoRN/algebra/CPoly_ApZero/Cpoly_choose_apzero.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/Cpoly_choose_apzero.con". (* UNEXPORTED -End Poly_Representation. +End Poly_Representation *) (* UNEXPORTED -Section Characteristic_zero. +Section Characteristic_zero *) (*#* @@ -142,28 +140,32 @@ If we are in a field of characteristic zero, the previous result can be strengthened. *) -inline cic:/CoRN/algebra/CPoly_ApZero/R.var. +alias id "R" = "cic:/CoRN/algebra/CPoly_ApZero/Characteristic_zero/R.var". (* begin show *) -inline cic:/CoRN/algebra/CPoly_ApZero/H.var. +alias id "H" = "cic:/CoRN/algebra/CPoly_ApZero/Characteristic_zero/H.var". (* end show *) (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) -inline cic:/CoRN/algebra/CPoly_ApZero/poly_apzero.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_apzero.con". (*#* Also, in this situation polynomials are extensional functions. *) -inline cic:/CoRN/algebra/CPoly_ApZero/poly_extensional.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/poly_extensional.con". (* UNEXPORTED -End Characteristic_zero. +End Characteristic_zero *) (*#* @@ -171,18 +173,22 @@ End Characteristic_zero. *) (* UNEXPORTED -Section Poly_ApZero_Interval. +Section Poly_ApZero_Interval *) -inline cic:/CoRN/algebra/CPoly_ApZero/R.var. +alias id "R" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_ApZero_Interval/R.var". (* begin hide *) +(* NOTATION +Notation RX := (cpoly_cring R). +*) + (* end hide *) -inline cic:/CoRN/algebra/CPoly_ApZero/Cpoly_apzero_interval.con. +inline "cic:/CoRN/algebra/CPoly_ApZero/Cpoly_apzero_interval.con". (* UNEXPORTED -End Poly_ApZero_Interval. +End Poly_ApZero_Interval *)