Theorems · Theorem · commutative algebra

LaurentSeries.tendsto_valuation

∀ (K : Type u_2) [inst : Field K]
  (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion (RatFunc K) (Polynomial.idealX K)),
  Filter.Tendsto (⇑Valued.v)
    (Filter.comap
      (fun x =>
        {
          toCompletion :=
            ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K))).symm
                x) })
      (nhds a))
    (nhds (Valued.v a))

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

0 results in Mathlib

Foundations

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

Assumes

Field