diff options
| author | Cyril Cohen | 2020-08-25 00:16:27 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-03 15:59:50 +0200 |
| commit | bb3f93b646a1a36e591a6837785e63cce7a4fa4e (patch) | |
| tree | 1cfc64e2ee4e3dde4bc19ed51ae1cc4ca31f5ac0 /mathcomp/algebra | |
| parent | d3950a35fe2e901d92335ae9c05562b14d049214 (diff) | |
Lemmas mxminpoly_minP and dvd_mxminpoly
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 9 |
1 files changed, 9 insertions, 0 deletions
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 /=. |