Theorems · Theorem · commutative algebra

PowerSeries.IsWeierstrassFactorization.elim

∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [IsHausdorff (IsLocalRing.maximalIdeal A) A]
  {g : PowerSeries A} {f f' : Polynomial A} {h h' : PowerSeries A},
  g.IsWeierstrassFactorization f h → g.IsWeierstrassFactorization f' h' → f = f' ∧ h = h'

The f and h in the Weierstrass preparation theorem are unique. This result is stated using two PowerSeries.IsWeierstrassFactorization assertions, and only requires the ring being Hausdorff with respect to the maximal ideal. If you want f and h equal to PowerSeries.weierstrassDistinguished and PowerSeries.weierstrassUnit, use PowerSeries.IsWeierstrassFactorization.unique instead, which requires the ring being complete with respect to the maximal ideal.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingIsLocalRingIsHausdorff