Theorems · Theorem · commutative algebra

PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal

∀ {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

Defined in

Mathlib.RingTheory.PowerSeries.CoeffMulMem

Cited by

4 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring