Some basic facts on polynomials + fix theory cloning for Poly

theories/algebra/Poly.ec

@@ -251,6 +251,17 @@ proof. by apply/poly_eqP=> i ge0_i; rewrite !coeffpE mul0r. qed.
 lemma scalep0 c : c ** poly0 = poly0.
 proof. by apply/poly_eqP=> i ge0_i; rewrite !coeffpE mulr0. qed.
 
+(* -------------------------------------------------------------------- *)
+lemma scale1p p : oner ** p = p.
+proof. by apply/poly_eqP=> i ge0_i; rewrite !coeffpE mul1r. qed.
+
+(* -------------------------------------------------------------------- *)
+lemma scalep1 c : c ** poly1 = polyC c.
+proof.
+apply/poly_eqP=> i ge0_i; rewrite !coeffpE !polyCE.
+by case: (i = 0) => _; [rewrite mulr1|rewrite mulr0].
+qed.
+
 (* -------------------------------------------------------------------- *)
 lemma scaleNp (c : coeff) p : (-c) ** p = - (c ** p).
 proof. by apply/poly_eqP=> i ge0_i; rewrite !coeffpE mulNr. qed.
@@ -849,9 +860,11 @@ type coeff.
 clone import IDomain as IDCoeff with type t <= coeff.
 
 clone include PolyComRing with
-  type coeff        <- coeff,
-  theory Coeff      <- IDCoeff.
-
+  type coeff   <- coeff,
+  theory Coeff <- IDCoeff,
+  op PolyComRing.invr (p : poly) =
+    (if deg p = 1 then polyC (IDCoeff.invr p.[0]) else p).
+
 clear [PolyComRing.* PolyComRing.AddMonoid.* PolyComRing.MulMonoid.*].
 
 import BigCf.
@@ -868,6 +881,7 @@ qed.
 pred unitp (p : poly) =
   deg p = 1 /\ IDCoeff.unit p.[0].
 
+(* -------------------------------------------------------------------- *)
 op polyV (p : poly) =
   if deg p = 1 then polyC (IDCoeff.invr p.[0]) else p.
 
@@ -880,6 +894,7 @@ clone import Ring.IDomain as IDPoly with
     op [ - ]  <- polyN,
     op ( * )  <- polyM,
     op invr   <- polyV,
+    op exp    <- PolyComRing.exp,
   pred unit   <- unitp
 
   proof *