Theorems · Definition · commutative algebra

PowerSeries.IsWeierstrassDivisorAt.divCoeff

{A : Type u_1} →
  [inst : CommRing A] →
    {g : PowerSeries A} →
      {I : Ideal A} →
        (H : g.IsWeierstrassDivisorAt I) →
          (f : PowerSeries A) →
            [IsPrecomplete I A] → (i : ℕ) → { x // ∀ (n : ℕ), (PowerSeries.coeff i) (H.seq f n) ≡ x [SMOD I ^ n • ⊤] }

The (bundled version of) coefficient of the limit q of the inductively constructed sequence qₖ in the proof of Weierstrass division.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingIsPrecomplete