second half of algebra backports

Author: Tragicus

theories/xmathcomp/various.v

@@ -108,17 +108,6 @@ Qed.
 (* package algebra *)
 (*******************)
 
-(**********)
-(* ssrint *)
-(**********)
-
-Lemma dvdz_charf (R : ringType) (p : nat) :
-  p \in [char R] -> forall n : int, (p %| n)%Z = (n%:~R == 0 :> R).
-Proof.
-move=> charRp [] n; rewrite [LHS](dvdn_charf charRp)//.
-by rewrite NegzE abszN rmorphN// oppr_eq0.
-Qed.
-
 (********)
 (* poly *)
 (********)
@@ -165,185 +154,6 @@ move=> /prim_expr_order/esym/eqP.
 by rewrite expr0n; case: (n =P 0%N); rewrite ?oner_eq0.
 Qed.
 
-(**********)
-(* intdiv *)
-(**********)
-
-Lemma eisenstein (p : nat) (q : {poly int}) : prime p -> (size q != 1)%N ->
-  (~~ (p %| lead_coef q))%Z -> (~~ ((p : int) ^+ 2 %| q`_0))%Z ->
-  (forall i, (i < (size q).-1)%N -> p %| q`_i)%Z ->
-  irreducible_poly (map_poly (intr : int -> rat) q).
-Proof.
-move=> p_prime qN1 Ndvd_pql Ndvd_pq0 dvd_pq.
-have qN0 : q != 0 by rewrite -lead_coef_eq0; apply: contraNneq Ndvd_pql => ->.
-split.
-   rewrite size_map_poly_id0 ?intr_eq0 ?lead_coef_eq0//.
-   by rewrite ltn_neqAle eq_sym qN1 size_poly_gt0.
-move=> f' +/dvdpP_rat_int[f [d dN0 feq]]; rewrite {f'}feq size_scale// => fN1.
-move=> /= [g q_eq]; rewrite q_eq (eqp_trans (eqp_scale _ _))//.
-have fN0 : f != 0 by apply: contra_neq qN0; rewrite q_eq => ->; rewrite mul0r.
-have gN0 : g != 0 by apply: contra_neq qN0; rewrite q_eq => ->; rewrite mulr0.
-rewrite size_map_poly_id0 ?intr_eq0 ?lead_coef_eq0// in fN1.
-have [/eqP/size_poly1P[c cN0 ->]|gN1] := eqVneq (size g) 1%N.
-  by rewrite mulrC mul_polyC map_polyZ/= eqp_sym eqp_scale// intr_eq0.
-have c_neq0 : (lead_coef q)%:~R != 0 :> 'F_p
-   by rewrite -(dvdz_charf (char_Fp _)).
-have : map_poly (intr : int -> 'F_p) q = (lead_coef q)%:~R *: 'X^(size q).-1.
-  apply/val_inj/(@eq_from_nth _ 0) => [|i]; rewrite size_map_poly_id0//.
-    by rewrite size_scale// size_polyXn -polySpred.
-  move=> i_small; rewrite coef_poly i_small coefZ coefXn lead_coefE.
-  move: i_small; rewrite polySpred// ltnS/=.
-  case: ltngtP => // [i_lt|->]; rewrite (mulr1, mulr0)//= => _.
-  by apply/eqP; rewrite -(dvdz_charf (char_Fp _))// dvd_pq.
-rewrite [in LHS]q_eq rmorphM/=.
-set c := (X in X *: _); set n := (_.-1).
-set pf := map_poly _ f; set pg := map_poly _ g => pfMpg.
-have dvdXn (r : {poly _}) : size r != 1%N -> r %| c *: 'X^n -> r`_0 = 0.
-  move=> rN1; rewrite (eqp_dvdr _ (eqp_scale _ _))//.
-  rewrite -['X]subr0; move=> /dvdp_exp_XsubC[k lekn]; rewrite subr0.
-  move=> /eqpP[u /andP[u1N0 u2N0]]; have [->|k_gt0] := posnP k.
-    move=> /(congr1 (size \o val))/eqP.
-    by rewrite /= !size_scale// size_polyXn (negPf rN1).
-  move=> /(congr1 (fun p : {poly _} => p`_0))/eqP.
-  by rewrite !coefZ coefXn ltn_eqF// mulr0 mulf_eq0 (negPf u1N0) => /eqP.
-suff : ((p : int) ^+ 2 %| q`_0)%Z by rewrite (negPf Ndvd_pq0).
-have := c_neq0; rewrite q_eq coefM big_ord1.
-rewrite lead_coefM rmorphM mulf_eq0 negb_or => /andP[lpfN0 qfN0].
-have pfN1 : size pf != 1%N by rewrite size_map_poly_id0.
-have pgN1 : size pg != 1%N by rewrite size_map_poly_id0.
-have /(dvdXn _ pgN1) /eqP : pg %| c *: 'X^n by rewrite -pfMpg dvdp_mull.
-have /(dvdXn _ pfN1) /eqP : pf %| c *: 'X^n by rewrite -pfMpg dvdp_mulr.
-by rewrite !coef_map// -!(dvdz_charf (char_Fp _))//; apply: dvdz_mul.
-Qed.
-
-(***********)
-(* polydiv *)
-(***********)
-Lemma irredp_XaddC (F : fieldType) (x : F) : irreducible_poly ('X + x%:P).
-Proof. by rewrite -[x]opprK rmorphN; apply: irredp_XsubC. Qed.
-
-Lemma eqpW (R : idomainType) (p q : {poly R}) : p = q -> p %= q.
-Proof. by move->; rewrite eqpxx. Qed.
-
-Lemma horner_mod (R : fieldType) (p q : {poly R}) x : root q x ->
-  (p %% q).[x] = p.[x].
-Proof.
-by move=> /eqP qx0; rewrite [p in RHS](divp_eq p q) !hornerE qx0 mulr0 add0r.
-Qed.
-
-Lemma root_dvdp (F : idomainType) (p q : {poly F}) (x : F) :
-  root p x -> p %| q -> root q x.
-Proof. rewrite -!dvdp_XsubCl; exact: dvdp_trans. Qed.
-
-Section multiplicity.
-Variable (L : fieldType).
-
-Definition mup (x : L) (p : {poly L}) :=
-  [arg max_(n > (0 : 'I_(size p).+1) | ('X - x%:P) ^+ n %| p) n] : nat.
-
-Lemma mup_geq x q n : q != 0 -> (n <= mup x q)%N = (('X - x%:P) ^+ n %| q).
-Proof.
-move=> q_neq0; rewrite /mup; symmetry.
-case: arg_maxnP; rewrite ?expr0 ?dvd1p//= => i i_dvd gti.
-case: ltnP => [|/dvdp_exp2l/dvdp_trans]; last exact.
-apply: contraTF => dvdq; rewrite -leqNgt.
-suff n_small : (n < (size q).+1)%N by exact: (gti (Ordinal n_small)).
-by rewrite ltnS ltnW// -(size_exp_XsubC _ x) dvdp_leq.
-Qed.
-
-Lemma mup_leq x q n : q != 0 -> (mup x q <= n)%N = ~~ (('X - x%:P) ^+ n.+1 %| q).
-Proof. by move=> qN0; rewrite leqNgt mup_geq. Qed.
-
-Lemma mup_ltn x q n : q != 0 -> (mup x q < n)%N = ~~ (('X - x%:P) ^+ n %| q).
-Proof. by move=> qN0; rewrite ltnNge mup_geq. Qed.
-
-Lemma XsubC_dvd x q : q != 0 -> ('X - x%:P %| q) = (0 < mup x q)%N.
-Proof. by move=> /mup_geq-/(_ _ 1%N)/esym; apply. Qed.
-
-Lemma mup_XsubCX n (x y : L) :
-  mup x (('X - y%:P) ^+ n) = (if (y == x) then n else 0)%N.
-Proof.
-have Xxn0 : ('X - y%:P) ^+ n != 0 by rewrite ?expf_neq0 ?polyXsubC_eq0.
-apply/eqP; rewrite eqn_leq mup_leq ?mup_geq//.
-have [->|Nxy] := eqVneq x y.
-  by rewrite /= dvdpp ?dvdp_Pexp2l ?size_XsubC ?ltnn.
-by rewrite dvd1p dvdp_XsubCl /root !hornerE ?horner_exp ?hornerE expf_neq0// subr_eq0.
-(* FIXME: remove ?horner_exp ?hornerE when requiring MC >= 1.16.0 *)
-Qed.
-
-Lemma mupNroot (x : L) q : ~~ root q x -> mup x q = 0%N.
-Proof.
-move=> qNx; have qN0 : q != 0 by apply: contraNneq qNx => ->; rewrite root0.
-by move: qNx; rewrite -dvdp_XsubCl XsubC_dvd// lt0n negbK => /eqP.
-Qed.
-
-Lemma mupMl x q1 q2 : ~~ root q1 x -> mup x (q1 * q2) = mup x q2.
-Proof.
-move=> q1Nx; have q1N0 : q1 != 0 by apply: contraNneq q1Nx => ->; rewrite root0.
-have [->|q2N0] := eqVneq q2 0; first by rewrite mulr0.
-apply/esym/eqP; rewrite eqn_leq mup_geq ?mulf_neq0// dvdp_mull -?mup_geq//=.
-rewrite mup_leq ?mulf_neq0// Gauss_dvdpr -?mup_ltn//.
-by rewrite coprimep_expl// coprimep_sym coprimep_XsubC.
-Qed.
-
-Lemma mupM x q1 q2 : q1 != 0 -> q2 != 0 ->
-   mup x (q1 * q2) = (mup x q1 + mup x q2)%N.
-Proof.
-move=> q1N0 q2N0; apply/eqP; rewrite eqn_leq mup_leq ?mulf_neq0//.
-rewrite mup_geq ?mulf_neq0// exprD ?dvdp_mul; do ?by rewrite -mup_geq.
-have [m1 [r1]] := multiplicity_XsubC q1 x; rewrite q1N0 /= => r1Nx ->.
-have [m2 [r2]] := multiplicity_XsubC q2 x; rewrite q2N0 /= => r2Nx ->.
-rewrite !mupMl// ?mup_XsubCX eqxx/= mulrACA exprS exprD.
-rewrite dvdp_mul2r ?mulf_neq0 ?expf_neq0 ?polyXsubC_eq0//.
-by rewrite dvdp_XsubCl rootM negb_or r1Nx r2Nx.
-Qed.
-
-Lemma mu_prod_XsubC (x : L) (s : seq L) :
-   mup x (\prod_(x <- s) ('X - x%:P)) = count_mem x s.
-Proof.
-elim: s => [|y s IHs]; rewrite (big_cons, big_nil)/=.
-  by rewrite mupNroot// root1.
-rewrite mupM ?polyXsubC_eq0// ?monic_neq0 ?monic_prod_XsubC//.
-by rewrite IHs (@mup_XsubCX 1).
-Qed.
-
-Lemma prod_XsubC_eq (s t : seq L) :
-  \prod_(x <- s) ('X - x%:P) = \prod_(x <- t) ('X - x%:P) -> perm_eq s t.
-Proof.
-move=> eq_prod; apply/allP => x _ /=; apply/eqP.
-by have /(congr1 (mup x)) := eq_prod; rewrite !mu_prod_XsubC.
-Qed.
-
-End multiplicity.
-
-Lemma dvdp_exp_XsubC (R : idomainType) (p : {poly R}) (c : R) n :
-  reflect (exists2 k, (k <= n)%N & p %= ('X - c%:P) ^+ k)
-          (p %| ('X - c%:P) ^+ n).
-Proof.
-apply: (iffP idP) => [|[k lkn /eqp_dvdl->]]; last by rewrite dvdp_exp2l.
-move=> /Pdiv.WeakIdomain.dvdpP[[/= a q] a_neq0].
-have [m [r]] := multiplicity_XsubC p c; have [->|pN0]/= := eqVneq p 0.
-  rewrite mulr0 => _ _ /eqP;  rewrite scale_poly_eq0 (negPf a_neq0)/=.
-  by rewrite expf_eq0/= andbC polyXsubC_eq0.
-move=> rNc ->; rewrite mulrA => eq_qrm; exists m.
-  have: ('X - c%:P) ^+ m %| a *: ('X - c%:P) ^+ n by rewrite eq_qrm dvdp_mull.
-  by rewrite (eqp_dvdr _ (eqp_scale _ _))// dvdp_Pexp2l// size_XsubC.
-suff /eqP : size r = 1%N.
-  by rewrite size_poly_eq1 => /eqp_mulr/eqp_trans->//; rewrite mul1r eqpxx.
-have : r %| a *: ('X - c%:P) ^+ n by rewrite eq_qrm mulrAC dvdp_mull.
-rewrite (eqp_dvdr _ (eqp_scale _ _))//.
-move: rNc; rewrite -coprimep_XsubC => /(coprimep_expr n) /coprimepP.
-by move=> /(_ _ (dvdpp _)); rewrite -size_poly_eq1 => /(_ _)/eqP.
-Qed.
-
-(**********)
-(* vector *)
-(**********)
-
-Lemma SubvsE (F0 : fieldType) (L : vectType F0) (k : {vspace L}) x (xk : x \in k) :
-  Subvs xk = vsproj k x.
-Proof. by apply/val_inj; rewrite /= vsprojK. Qed.
-
 (*****************)
 (* package field *)
 (*****************)