diff options
| author | Laurent Théry | 2020-09-03 13:15:42 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-03 13:15:42 +0200 |
| commit | b392a135a5f69a91526ce8004bb29659ef4be511 (patch) | |
| tree | 74949ce400f10a487b15b065e2356f78bf6d155f | |
| parent | 8354303bc6ef26ff92e923df60cb190fbedee984 (diff) | |
| parent | 31978e486f48b902d18c5f508e34bc016d7f47b8 (diff) | |
Merge pull request #560 from CohenCyril/commr_horner
Adding commr_horner lemma
| -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. |