∀ (K : Type u_2) [inst : Field K],
  Subring.map (LaurentSeries.LaurentSeriesRingEquiv K).toRingHom (LaurentSeries.powerSeries_as_subring K) =
    (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K)).toSubring