Theorems · Definition · commutative algebra

PowerSeries.weierstrassMod

{A : Type u_1} →
  [inst : CommRing A] →
    [inst_1 : IsLocalRing A] →
      PowerSeries A → PowerSeries A → [IsPrecomplete (IsLocalRing.maximalIdeal A) A] → Polynomial A

The remainder r in Weierstrass division, denoted by f %ʷ g. Note that when the image of g in the residue field is zero, this is defined to be zero.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

11 results in Mathlib

Foundations

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

Assumes

CommRingIsLocalRingIsPrecomplete