Theorems · Theorem · commutative algebra

PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply

∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A}
  (H : g.IsWeierstrassFactorizationAt f h I) [inst_1 : IsAdicComplete I A] (x : PowerSeries A ⧸ Ideal.span {g}),
  H.algEquivQuotient.symm x = (Ideal.Quotient.mk (Ideal.span {f})) (⋯.mod' ((Ideal.quotientEquivAlgOfEq A ⋯) x))

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsAdicComplete