diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 1 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5a394b5..536a9f9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -59,6 +59,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + lemmas `allrel_map`, `allrelP` and `allrel0`. + lemmas `allrel1`, `allrel2` and `allrel_cons`, under assumptions of reflexivity and symmetry of `r`. +- in `mxpoly.v`, new lemmas `mxminpoly_minP` and `dvd_mxminpoly`. ### Changed diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index a8cf94b..cbac070 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -598,6 +598,15 @@ Qed. Lemma mxminpoly_min p : horner_mx A p = 0 -> p_A %| p. Proof. by move=> pA0; rewrite /dvdp -horner_mxK pA0 mx_inv_horner0. Qed. +Lemma mxminpoly_minP p : reflect (horner_mx A p = 0) (p_A %| p). +Proof. +apply: (iffP idP); last exact: mxminpoly_min. +by move=> /Pdiv.Field.dvdpP[q ->]; rewrite rmorphM/= mx_root_minpoly mulr0. +Qed. + +Lemma dvd_mxminpoly p : (p_A %| p) = (horner_mx A p == 0). +Proof. exact/mxminpoly_minP/eqP. Qed. + Lemma horner_rVpoly_inj : injective (horner_mx A \o rVpoly : 'rV_d -> 'M_n). Proof. apply: can_inj (poly_rV \o mx_inv_horner) _ => u /=. |