(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* This file was automatically generated: do not edit *********************)

include "CoRN.ma".

(* $Id: CPoly_ApZero.v,v 1.3 2004/04/23 10:00:53 lcf Exp $ *)

include "algebra/CPoly_Degree.ma".

include "algebra/COrdFields2.ma".

(*#* * Polynomials apart from zero *)

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/distinct1.con" as definition.

(* UNEXPORTED
Implicit Arguments distinct1 [A].
*)

(* UNEXPORTED
Section Poly_Representation
*)

(*#*
** Representation of polynomials
%\begin{convention}% Let [R] be a field, [RX] the ring of polynomials
over [R], [a_ : nat->R] with [(distinct1 a_)] and let [f] be a
polynomial over [R], [n] a natural with [(degree_le n f)], i.e. [f]
has degree at most [n].
%\end{convention}%
*)

(* UNEXPORTED
cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/R.var
*)

(* UNEXPORTED
cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/a_.var
*)

(* UNEXPORTED
cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/distinct_a_.var
*)

(* UNEXPORTED
cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/f.var
*)

(* UNEXPORTED
cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/n.var
*)

(* UNEXPORTED
cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/degree_f.var
*)

(* begin hide *)

(* NOTATION
Notation RX := (cpoly_cring R).
*)

(* end hide *)

include "tactics/Transparent_algebra.ma".

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_linear_shifted.con" as lemma.

include "tactics/Opaque_algebra.ma".

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_linear_factor.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/zero_poly.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/identical_poly.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'.con" as definition.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_degree.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_zero.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_apzero.con" as lemma.

(* UNEXPORTED
Hint Resolve poly_01_factor'_zero.
*)

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor.con" as definition.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_degree.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_zero.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_one.con" as lemma.

(* UNEXPORTED
Hint Resolve poly_01_factor_zero poly_01_factor_one: algebra.
*)

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01.con" as definition.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree'.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_zero.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_one.con" as lemma.

(* UNEXPORTED
Hint Resolve poly_01_zero poly_01_one: algebra.
*)

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_representation''.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_representation'.con" as lemma.

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_representation.con" as lemma.

(* UNEXPORTED
Hint Resolve poly_representation: algebra.
*)

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/Cpoly_choose_apzero.con" as lemma.

(* UNEXPORTED
End Poly_Representation
*)

(* UNEXPORTED
Section Characteristic_zero
*)

(*#*
If we are in a field of characteristic zero, the previous result can be
strengthened.
*)

(* UNEXPORTED
cic:/CoRN/algebra/CPoly_ApZero/Characteristic_zero/R.var
*)

(* begin show *)

(* UNEXPORTED
cic:/CoRN/algebra/CPoly_ApZero/Characteristic_zero/H.var
*)

(* end show *)

(* begin hide *)

(* NOTATION
Notation RX := (cpoly_cring R).
*)

(* end hide *)

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_apzero.con" as lemma.

(*#*
Also, in this situation polynomials are extensional functions.
*)

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_extensional.con" as lemma.

(* UNEXPORTED
End Characteristic_zero
*)

(*#*
** Polynomials are nonzero on any interval
*)

(* UNEXPORTED
Section Poly_ApZero_Interval
*)

(* UNEXPORTED
cic:/CoRN/algebra/CPoly_ApZero/Poly_ApZero_Interval/R.var
*)

(* begin hide *)

(* NOTATION
Notation RX := (cpoly_cring R).
*)

(* end hide *)

inline procedural "cic:/CoRN/algebra/CPoly_ApZero/Cpoly_apzero_interval.con" as lemma.

(* UNEXPORTED
End Poly_ApZero_Interval
*)