diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 6 |
2 files changed, 8 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0309630..3347f21 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -41,6 +41,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `cV0Pn` to characterize nonzero matrices and find a nonzero coefficient. +- in `poly.v`, new lemma `commr_horner`. + ### Changed - in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index e83bc09..a33788d 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1093,6 +1093,12 @@ Proof. by rewrite /comm_poly !hornerC !simp. Qed. Lemma comm_polyX x : comm_poly 'X x. Proof. by rewrite /comm_poly !hornerX. Qed. +Lemma commr_horner a b p : GRing.comm a b -> comm_coef p a -> GRing.comm a p.[b]. +Proof. +move=> cab cpa; rewrite horner_coef; apply: commr_sum => i _. +by apply: commrM => //; apply: commrX. +Qed. + Lemma hornerM_comm p q x : comm_poly q x -> (p * q).[x] = p.[x] * q.[x]. Proof. move=> comm_qx. |