[isabelle] HOL/Library/Polynomial pcompose



the definition

  definition pcompose :: "'a::comm_semiring_0 poly => 'a poly => 'a poly"
  where
    "pcompose p q = fold_coeffs (λa c. [:a:] + q * c) p 0"


is not yet used --- what is the purpose of it ?
Walther




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.