diff options
| author | Cyril Cohen | 2020-10-30 18:50:56 +0100 |
|---|---|---|
| committer | GitHub | 2020-10-30 18:50:56 +0100 |
| commit | 1ec04efdcd1b00a6ae651551699c8b815a2a063f (patch) | |
| tree | 62f0dc367dc9ab3fa4210ee5e003b03a34eda25f /mathcomp/algebra/mxpoly.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
| parent | bd02346e4038871f4d4021dd84df384fc8cf9aa4 (diff) | |
Merge pull request #607 from pi8027/distr-suffixes
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/algebra/mxpoly.v')
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 74d524e..c7f8fb1 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -890,7 +890,7 @@ rewrite !big_cons; case: ifP => [Pj|PNj]; rewrite ?ihjs ?submx_refl//. suff cjjs: coprimep (p_ j) (\prod_(i <- js | P i) p_ i). by rewrite !kermxpolyM// !(adds_eqmx (eqmx_refl _) (ihjs _)) ?submx_refl. rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first. - by move=> p q; rewrite coprimep_mulr. + by move=> p q; rewrite coprimepMr. apply/allP => i i_js; apply/implyP => Pi; apply: p_coprime => //. by apply: contraNneq jNjs => <-. Qed. @@ -907,7 +907,7 @@ have cpNi : {in [pred j | P j && (j != i)] &, rewrite -!(cap_eqmx (eqmx_refl _) (kermxpoly_prod g _))//. rewrite mxdirect_kermxpoly ?submx_refl//. rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first. - by move=> p q; rewrite coprimep_mulr. + by move=> p q; rewrite coprimepMr. by apply/allP => j _; apply/implyP => /andP[Pj neq_ji]; apply: p_coprime. Qed. |