X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCPoly_ApZero.ma;h=5878f166315d19927e0af06cbaf29594acf4e14a;hb=62596f4e0a109e43c9df5da20571827c8b905ce4;hp=d6839ae4043087122bfa3385adcc9758f945ba1c;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma b/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma index d6839ae40..5878f1663 100644 --- a/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma +++ b/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. +inline "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/R.var" "Poly_Representation__". -inline cic:/CoRN/algebra/CPoly_ApZero/a_.var. +inline "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/a_.var" "Poly_Representation__". -inline cic:/CoRN/algebra/CPoly_ApZero/distinct_a_.var. +inline "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/distinct_a_.var" "Poly_Representation__". -inline cic:/CoRN/algebra/CPoly_ApZero/f.var. +inline "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/f.var" "Poly_Representation__". -inline cic:/CoRN/algebra/CPoly_ApZero/n.var. +inline "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/n.var" "Poly_Representation__". -inline cic:/CoRN/algebra/CPoly_ApZero/degree_f.var. +inline "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/degree_f.var" "Poly_Representation__". (* 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. +inline "cic:/CoRN/algebra/CPoly_ApZero/Characteristic_zero/R.var" "Characteristic_zero__". (* begin show *) -inline cic:/CoRN/algebra/CPoly_ApZero/H.var. +inline "cic:/CoRN/algebra/CPoly_ApZero/Characteristic_zero/H.var" "Characteristic_zero__". (* 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. +inline "cic:/CoRN/algebra/CPoly_ApZero/Poly_ApZero_Interval/R.var" "Poly_ApZero_Interval__". (* 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 *)