Theorems · Theorem · commutative algebra

PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision

∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A}
  (H : g.IsWeierstrassFactorization f h),
  (PowerSeries.X ^ ((PowerSeries.map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g (↑⋯.unit⁻¹)
    (Polynomial.X ^ ((PowerSeries.map (IsLocalRing.residue A)) g).order.toNat - f)

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsLocalRing