Theorems · Theorem · commutative algebra

PowerSeries.weierstrassDistinguished_mul

∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A]
  {g g' : PowerSeries A} (hg : (PowerSeries.map (IsLocalRing.residue A)) (g * g') ≠ 0),
  (g * g').weierstrassDistinguished hg = g.weierstrassDistinguished ⋯ * g'.weierstrassDistinguished ⋯

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsLocalRingIsAdicComplete