diff options
| author | Kazuhiko Sakaguchi | 2020-10-09 00:21:00 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-29 12:31:31 +0900 |
| commit | c6e0d703165b0c60c270672eb542aa8934929bfe (patch) | |
| tree | 3ce1b05b861ca60e88bc7ab8b5226b12a879e3e6 /mathcomp/algebra/mxpoly.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/algebra/mxpoly.v')
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 74d524e..acf0e95 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. @@ -938,7 +938,7 @@ Lemma mxdirect_sum_geigenspace {in P &, injective a_} -> mxdirect (\sum_(i | P i) geigenspace g (a_ i)). Proof. move=> /inj_in_eq eq_a; apply: mxdirect_sum_kermx => i j Pi Pj Nji. -by rewrite coprimep_expr ?coprimep_expl// coprimep_XsubC root_XsubC eq_a. +by rewrite coprimepXr ?coprimepXl// coprimep_XsubC root_XsubC eq_a. Qed. Definition eigenpoly n (g : 'M_n) : pred {poly K} := |