∀ {A : Type u_1} [inst : Semiring A] {I J : Ideal A} {f g : PowerSeries A} (n : ℕ),
  (∀ i ≤ n, (PowerSeries.coeff i) f ∈ I) →
    (∀ i ≤ n, (PowerSeries.coeff i) g ∈ J) → ∀ i ≤ n, (PowerSeries.coeff i) (f * g) ∈ I * J