diff options
Diffstat (limited to 'mathcomp/algebra/poly.v')
| -rw-r--r-- | mathcomp/algebra/poly.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index d21e690..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. @@ -1700,7 +1706,7 @@ Arguments rootP {R p x}. Arguments rootPf {R p x}. Arguments rootPt {R p x}. Arguments unity_rootP {R n z}. -Arguments polyOverP {R S0 addS kS p}. +Arguments polyOverP {R S0 addS kS p} : rename. Arguments polyC_inj {R} [x1 x2] eq_x12P. Arguments eq_poly {R n} [E1] E2 eq_E12. |