# Library closed_poly

This file contains facts about polynomials with coefficients in a closed field. In what follows, we pose p = (X - r1)^+a1 * (X - r2)^+a2 * ... * (X - rn)^+an root_seq p == the sequence of all roots of polynomial p. i.e. [:: r1; r1; ...; r2; r2; ...; rn; ... rn] or a permutation of this sequence root_seq_uniq p == the sequence of all distinct roots of polynomial p (i.e the sequence [:: r1; ...; rn]) root_mu_seq p == the sequence of pair off the roots and their multiplicity in polynomial p. (i.e the sequence [:: (r1,a1); ... ; (rn,an) ]) root_seq_poly s == the concatenation of the sequences root_mu_seq p for all polynomials p in the sequence s. linear_factor_seq p == the sequence of linear factors that appear in the decomposition of polynomial p. (i.e the sequence [:: (X - r1)^+a1; ... ; (X - rn)^+an])

Set Implicit Arguments.

Section poly_closedFieldType.

Variable F : closedFieldType.
Import GRing.Theory.

Local Open Scope ring_scope.

Definition root_seq : {poly F} -> seq F :=
let fix loop (p : {poly F}) (n : nat) :=
if n is n.+1 then
if (size p != 1%N) =P true is ReflectT p_neq0
then let x := projT1 (sigW (closed_rootP p p_neq0)) in
x :: loop (p %/ ('X - x%:P)) n
else [::]
else [::]
in fun p => loop p (size p).

Lemma root_root_seq (p : {poly F}) x : p != 0 -> x \in root_seq p = root p x.

Lemma root_seq_cons (p : {poly F}) x s : root_seq p = x :: s ->
s = root_seq (p %/ ('X - x%:P)).

Lemma root_seq_eq (p : {poly F}) :
p = lead_coef p *: \prod_(x <- root_seq p) ('X - x%:P).

Lemma root_seq0 : root_seq 0 = [::].

Lemma size_root_seq p : size (root_seq p) = (size p).-1.

Lemma root_seq_nil (p : {poly F}) : (size p <= 1) = ((root_seq p) == [::]).

Lemma sub_root_div (p q : {poly F}) (Hq : q != 0) :
p %| q -> {subset (root_seq p) <= (root_seq q)} .

Definition root_seq_uniq p := undup (root_seq p).

Lemma prod_XsubC_count (p : {poly F}):
\prod_(x <- root_seq_uniq p) ('X - x%:P)^+ (count (pred1 x) (root_seq p)).

Lemma count_root_seq p x : count (pred1 x) (root_seq p) = \mu_x p.

Definition root_mu_seq p := [seq (x,(\mu_x p)) | x <- (root_seq_uniq p)].

Lemma root_mu_seq_pos x p : p != 0 -> x \in root_mu_seq p -> 0 < x.2.

Definition root_seq_poly (s : seq {poly F}) := flatten (map root_mu_seq s).

Lemma root_seq_poly_pos x s : (forall p , p \in s -> p !=0) ->
x \in root_seq_poly s -> 0 < x.2.

Definition linear_factor_seq p :=
[seq ('X - x.1%:P)^+x.2 | x <- (root_mu_seq p)].

Lemma monic_linear_factor_seq p : forall q, q \in linear_factor_seq p ->
q \is monic.

Lemma size_linear_factor_leq1 p : forall q, q \in linear_factor_seq p ->
1 < size q.

Lemma coprimep_linear_factor_seq p :
forall (i j : 'I_(size (linear_factor_seq p))),
i != j ->
coprimep (linear_factor_seq p)_i (linear_factor_seq p)_j.

Lemma prod_XsubC_mu (p : {poly F}):
p = (lead_coef p) *: \prod_(x <- root_seq_uniq p) ('X - x%:P)^+(\mu_x p).

Lemma monic_prod_XsubC p :
p \is monic -> p = \prod_(x <- root_seq_uniq p) ('X - x%:P)^+(\mu_x p).

Lemma prod_factor (p : {poly F}):
p = (lead_coef p) *: \prod_(x <- linear_factor_seq p) x.

Lemma monic_prod_factor p :
p \is monic -> p = \prod_(x <- linear_factor_seq p) x.

Lemma uniq_root_mu_seq (p : {poly F}) : uniq (root_seq p) ->
forall x, x \in root_mu_seq p -> x.2 = 1%N.

Lemma uniq_root_dvdp p q : q != 0 ->
(uniq (root_seq q)) -> p %| q -> (uniq (root_seq p)).

Lemma root_root_mu_seq p : [seq x.1 | x <- root_mu_seq p] = root_seq_uniq p.

End poly_closedFieldType.