Theorems · Definition · commutative algebra

PowerSeries.algEquivQuotientWeierstrassDistinguished

{A : Type u_1} →
  [inst : CommRing A] →
    [inst_1 : IsLocalRing A] →
      [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A] →
        {g : PowerSeries A} →
          (hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0) →
            (Polynomial A ⧸ Ideal.span {g.weierstrassDistinguished hg}) ≃ₐ[A] PowerSeries A ⧸ Ideal.span {g}

If g is a power series over a complete local ring, such that its image in the residue field is not zero, then there is a natural isomorphism A[X] / (f) ≃ₐ[A] A⟦X⟧ / (g) where f is PowerSeries.weierstrassDistinguished g.

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

CommRingIsLocalRingIsAdicComplete