Theorems · Theorem · commutative algebra

LaurentSeries.exists_powerSeries_of_memIntegers

∀ (K : Type u_2) [inst : Field K] {x : LaurentSeries.RatFuncAdicCompl K},
  x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K) →
    ∃ F, (LaurentSeries.LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) F) = x

Conversely, all elements in the unit ball inside the completion of K⟮X⟯ come from a power series through the isomorphism LaurentSeriesRingEquiv.

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field