Theorems · Theorem · commutative algebra

PowerSeries.IsWeierstrassFactorizationAt.mul

∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassFactorizationAt f h I →
    ∀ {g' : PowerSeries A} {f' : Polynomial A} {h' : PowerSeries A},
      g'.IsWeierstrassFactorizationAt f' h' I → (g * g').IsWeierstrassFactorizationAt (f * f') (h * h') I

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing