From 28a26e79bcdc7abec01a4ac4c1922798abf0f24a Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 28 Mar 2024 16:53:58 +0100 Subject: [PATCH] second half of algebra backports --- theories/xmathcomp/various.v | 190 ----------------------------------- 1 file changed, 190 deletions(-) diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index d76b84e..4af605e 100644 --- a/theories/xmathcomp/various.v +++ b/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 *) (*****************)