Theorems · Definition · commutative algebra

PowerSeries.IsWeierstrassDivisorAt.mod

{A : Type u_1} →
  [inst : CommRing A] →
    {g : PowerSeries A} →
      {I : Ideal A} → g.IsWeierstrassDivisorAt I → PowerSeries A → [IsPrecomplete I A] → Polynomial A

The remainder r in the proof of Weierstrass division.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

16 results in Mathlib

Foundations

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

Assumes

CommRingIsPrecomplete