Laurent Series

In this file we define LaurentSeries R, the formal Laurent series over R, here an arbitrary type with a zero. They are denoted R⸨X⸩.

Main Definitions

• Defines LaurentSeries as an abbreviation for HahnSeries ℤ.
• Defines hasseDeriv of a Laurent series with coefficients in a module over a ring.
• Provides a coercion from power series R⟦X⟧ into R⸨X⸩ given by HahnSeries.ofPowerSeries.
• Defines LaurentSeries.powerSeriesPart
• Defines the localization map LaurentSeries.of_powerSeries_localization which evaluates to HahnSeries.ofPowerSeries.
• Embedding of rational functions into Laurent series, provided as a coercion, utilizing the underlying RatFunc.coeAlgHom.
• Study of the X-Adic valuation on the ring of Laurent series over a field
• In LaurentSeries.uniformContinuous_coeff we show that sending a Laurent series to its dth coefficient is uniformly continuous, ensuring that it sends a Cauchy filter ℱ in K⸨X⸩ to a Cauchy filter in K: since this latter is given the discrete topology, this provides an element LaurentSeries.Cauchy.coeff ℱ d in K that serves as dth coefficient of the Laurent series to which the filter ℱ converges.

Main Results

• Basic properties of Hasse derivatives

About the X-Adic valuation:

• The (integral) valuation of a power series is the order of the first non-zero coefficient, see LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero.
• The valuation of a Laurent series is the order of the first non-zero coefficient, see LaurentSeries.valuation_le_iff_coeff_lt_eq_zero.
• Every Laurent series of valuation less than (1 : ℤᵐ⁰) comes from a power series, see LaurentSeries.val_le_one_iff_eq_coe.
• The uniform space of LaurentSeries over a field is complete, formalized in the instance instLaurentSeriesComplete.
• The field of rational functions is dense in LaurentSeries: this is the declaration LaurentSeries.coe_range_dense and relies principally upon LaurentSeries.exists_ratFunc_val_lt, stating that for every Laurent series f and every γ : ℤᵐ⁰ one can find a rational function Q such that the X-adic valuation v satisfies v (f - Q) < γ.
• In LaurentSeries.valuation_compare we prove that the extension of the X-adic valuation from RatFunc K up to its abstract completion coincides, modulo the isomorphism with K⸨X⸩, with the X-adic valuation on K⸨X⸩.
• The two declarations LaurentSeries.mem_integers_of_powerSeries and LaurentSeries.exists_powerSeries_of_memIntegers show that an element in the completion of RatFunc K is in the unit ball if and only if it comes from a power series through the isomorphism LaurentSeriesRingEquiv.
• LaurentSeries.powerSeriesAlgEquiv is the K-algebra isomorphism between K⟦X⟧ and the unit ball inside the X-adic completion of RatFunc K.

Implementation details

• Since LaurentSeries is just an abbreviation of HahnSeries ℤ, the definition of the coefficients is given in terms of HahnSeries.coeff and this forces sometimes to go back-and-forth from X : R⸨X⸩ to single 1 1 : R⟦ℤ⟧.
• To prove the isomorphism between the X-adic completion of RatFunc K and K⸨X⸩ we construct two completions of RatFunc K: the first (LaurentSeries.ratfuncAdicComplPkg) is its abstract uniform completion; the second (LaurentSeries.LaurentSeriesPkg) is simply K⸨X⸩, once we prove that it is complete and contains RatFunc K as a dense subspace. The isomorphism is the comparison equivalence, expressing the mathematical idea that the completion "is unique". It is LaurentSeries.comparePkg.
• For applications to K⟦X⟧ it is actually more handy to use the inverse of the above equivalence: LaurentSeries.LaurentSeriesAlgEquiv is the topological, algebra equivalence K⸨X⸩ ≃ₐ[K] RatFuncAdicCompl K.
• In order to compare K⟦X⟧ with the valuation subring in the X-adic completion of RatFunc K we consider its alias LaurentSeries.powerSeries_as_subring as a subring of K⸨X⸩, that is itself clearly isomorphic (via the inverse of LaurentSeries.powerSeriesEquivSubring) to K⟦X⟧.

@[reducible, inline]

abbrev LaurentSeries (R : Type u) [Zero R] : Type u

LaurentSeries R is the type of formal Laurent series with coefficients in R, denoted R⸨X⸩.

It is implemented as a HahnSeries with value group ℤ.

def LaurentSeries.«term_⸨X⸩» : Lean.TrailingParserDescr

R⸨X⸩ is notation for LaurentSeries R.

def LaurentSeries.hasseDeriv (R : Type u_2) {V : Type u_3} [AddCommGroup V] [Semiring R] [Module R V] (k : ℕ) : LaurentSeries V →ₗ[R] LaurentSeries V

The Hasse derivative of Laurent series, as a linear map.

@[simp]

theorem LaurentSeries.hasseDeriv_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (f : LaurentSeries V) (n : ℤ) : ((hasseDeriv R k) f).coeff n = Ring.choose (n + ↑k) k • f.coeff (n + ↑k)

@[simp]

theorem LaurentSeries.hasseDeriv_zero {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] : hasseDeriv R 0 = LinearMap.id

theorem LaurentSeries.hasseDeriv_single_add {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (n : ℤ) (x : V) : (hasseDeriv R k) ((HahnSeries.single (n + ↑k)) x) = (HahnSeries.single n) (Ring.choose (n + ↑k) k • x)

@[simp]

theorem LaurentSeries.hasseDeriv_single {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (n : ℤ) (x : V) : (hasseDeriv R k) ((HahnSeries.single n) x) = (HahnSeries.single (n - ↑k)) (Ring.choose n k • x)

theorem LaurentSeries.hasseDeriv_comp_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k l : ℕ) (f : LaurentSeries V) (n : ℤ) : ((hasseDeriv R k) ((hasseDeriv R l) f)).coeff n = ((k + l).choose k • (hasseDeriv R (k + l)) f).coeff n

@[simp]

theorem LaurentSeries.hasseDeriv_comp {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k l : ℕ) (f : LaurentSeries V) : (hasseDeriv R k) ((hasseDeriv R l) f) = (k + l).choose k • (hasseDeriv R (k + l)) f

def LaurentSeries.derivative (R : Type u_3) {V : Type u_4} [AddCommGroup V] [Semiring R] [Module R V] : LaurentSeries V →ₗ[R] LaurentSeries V

The derivative of a Laurent series.

@[simp]

theorem LaurentSeries.derivative_apply {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (f : LaurentSeries V) : (derivative R) f = (hasseDeriv R 1) f

theorem LaurentSeries.derivative_iterate {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (f : LaurentSeries V) : (⇑(derivative R))^[k] f = k.factorial • (hasseDeriv R k) f

@[simp]

theorem LaurentSeries.derivative_iterate_coeff {R : Type u_1} [Semiring R] {V : Type u_2} [AddCommGroup V] [Module R V] (k : ℕ) (f : LaurentSeries V) (n : ℤ) : ((⇑(derivative R))^[k] f).coeff n = (descPochhammer ℤ k).smeval (n + ↑k) • f.coeff (n + ↑k)

instance LaurentSeries.instCoePowerSeries {R : Type u_1} [Semiring R] : Coe (PowerSeries R) (LaurentSeries R)

@[simp]

theorem LaurentSeries.coeff_coe_powerSeries {R : Type u_1} [Semiring R] (x : PowerSeries R) (n : ℕ) : ((HahnSeries.ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff n) x

def LaurentSeries.powerSeriesPart {R : Type u_1} [Semiring R] (x : LaurentSeries R) : PowerSeries R

This is a power series that can be multiplied by an integer power of X to give our Laurent series. If the Laurent series is nonzero, powerSeriesPart has a nonzero constant term.

@[simp]

theorem LaurentSeries.powerSeriesPart_coeff {R : Type u_1} [Semiring R] (x : LaurentSeries R) (n : ℕ) : (PowerSeries.coeff n) x.powerSeriesPart = x.coeff (HahnSeries.order x + ↑n)

@[simp]

theorem LaurentSeries.powerSeriesPart_zero {R : Type u_1} [Semiring R] : powerSeriesPart 0 = 0

@[simp]

theorem LaurentSeries.powerSeriesPart_eq_zero {R : Type u_1} [Semiring R] (x : LaurentSeries R) : x.powerSeriesPart = 0 ↔ x = 0

@[simp]

theorem LaurentSeries.single_order_mul_powerSeriesPart {R : Type u_1} [Semiring R] (x : LaurentSeries R) : (HahnSeries.single (HahnSeries.order x)) 1 * (HahnSeries.ofPowerSeries ℤ R) x.powerSeriesPart = x

theorem LaurentSeries.ofPowerSeries_powerSeriesPart {R : Type u_1} [Semiring R] (x : LaurentSeries R) : (HahnSeries.ofPowerSeries ℤ R) x.powerSeriesPart = (HahnSeries.single (-HahnSeries.order x)) 1 * x

theorem LaurentSeries.X_order_mul_powerSeriesPart {R : Type u_1} [Semiring R] {n : ℕ} {f : LaurentSeries R} (hn : ↑n = HahnSeries.order f) : (HahnSeries.ofPowerSeries ℤ R) (PowerSeries.X ^ n * f.powerSeriesPart) = f

instance LaurentSeries.instAlgebraPowerSeries {R : Type u_1} [CommSemiring R] : Algebra (PowerSeries R) (LaurentSeries R)

@[simp]

theorem LaurentSeries.coe_algebraMap {R : Type u_1} [CommSemiring R] : ⇑(algebraMap (PowerSeries R) (LaurentSeries R)) = ⇑(HahnSeries.ofPowerSeries ℤ R)

instance LaurentSeries.of_powerSeries_localization {R : Type u_1} [CommRing R] : IsLocalization (Submonoid.powers PowerSeries.X) (LaurentSeries R)

The localization map from power series to Laurent series.

instance LaurentSeries.instIsFractionRingPowerSeries {K : Type u_2} [Field K] : IsFractionRing (PowerSeries K) (LaurentSeries K)

theorem PowerSeries.coe_zero {R : Type u_1} [Semiring R] : (HahnSeries.ofPowerSeries ℤ R) 0 = 0

theorem PowerSeries.coe_one {R : Type u_1} [Semiring R] : (HahnSeries.ofPowerSeries ℤ R) 1 = 1

theorem PowerSeries.coe_add {R : Type u_1} [Semiring R] (f g : PowerSeries R) : (HahnSeries.ofPowerSeries ℤ R) (f + g) = (HahnSeries.ofPowerSeries ℤ R) f + (HahnSeries.ofPowerSeries ℤ R) g

theorem PowerSeries.coe_sub {R' : Type u_2} [Ring R'] (f' g' : PowerSeries R') : (HahnSeries.ofPowerSeries ℤ R') (f' - g') = (HahnSeries.ofPowerSeries ℤ R') f' - (HahnSeries.ofPowerSeries ℤ R') g'

theorem PowerSeries.coe_neg {R' : Type u_2} [Ring R'] (f' : PowerSeries R') : (HahnSeries.ofPowerSeries ℤ R') (-f') = -(HahnSeries.ofPowerSeries ℤ R') f'

theorem PowerSeries.coe_mul {R : Type u_1} [Semiring R] (f g : PowerSeries R) : (HahnSeries.ofPowerSeries ℤ R) (f * g) = (HahnSeries.ofPowerSeries ℤ R) f * (HahnSeries.ofPowerSeries ℤ R) g

theorem PowerSeries.coeff_coe {R : Type u_1} [Semiring R] (f : PowerSeries R) (i : ℤ) : ((HahnSeries.ofPowerSeries ℤ R) f).coeff i = if i < 0 then 0 else (coeff i.natAbs) f

theorem PowerSeries.coe_C {R : Type u_1} [Semiring R] (r : R) : (HahnSeries.ofPowerSeries ℤ R) (C r) = HahnSeries.C r

theorem PowerSeries.coe_X {R : Type u_1} [Semiring R] : (HahnSeries.ofPowerSeries ℤ R) X = (HahnSeries.single 1) 1

@[simp]

theorem PowerSeries.coe_smul {R : Type u_1} [Semiring R] {S : Type u_3} [Semiring S] [Module R S] (r : R) (x : PowerSeries S) : (HahnSeries.ofPowerSeries ℤ S) (r • x) = r • (HahnSeries.ofPowerSeries ℤ S) x

theorem PowerSeries.coe_pow {R : Type u_1} [Semiring R] (f : PowerSeries R) (n : ℕ) : (HahnSeries.ofPowerSeries ℤ R) (f ^ n) = (HahnSeries.ofPowerSeries ℤ R) f ^ n

instance RatFunc.instFaithfulSMulPolynomialLaurentSeries {F : Type u} [Field F] : FaithfulSMul (Polynomial F) (LaurentSeries F)

instance RatFunc.coeToLaurentSeries {F : Type u} [Field F] : Coe (RatFunc F) (LaurentSeries F)

theorem RatFunc.coe_coe {F : Type u} [Field F] (P : Polynomial F) : (HahnSeries.ofPowerSeries ℤ F) ↑P = (algebraMap (RatFunc F) (LaurentSeries F)) ↑P

@[simp]

theorem RatFunc.coe_X {F : Type u} [Field F] : (algebraMap (RatFunc F) (LaurentSeries F)) X = (HahnSeries.single 1) 1

theorem RatFunc.single_one_eq_pow {R : Type u_2} [Semiring R] (n : ℕ) : (HahnSeries.single ↑n) 1 = (HahnSeries.single 1) 1 ^ n

@[deprecated HahnSeries.inv_single (since := "2025-11-07")]

theorem RatFunc.single_inv {F : Type u} [Field F] (d : ℤ) {α : F} (hα : α ≠ 0) : (HahnSeries.single (-d)) α⁻¹ = ((HahnSeries.single d) α)⁻¹

theorem RatFunc.single_zpow {F : Type u} [Field F] (n : ℤ) : (HahnSeries.single n) 1 = (HahnSeries.single 1) 1 ^ n

theorem RatFunc.algebraMap_apply_div {F : Type u} [Field F] (p q : Polynomial F) : (algebraMap (RatFunc F) (LaurentSeries F)) ((algebraMap (Polynomial F) (RatFunc F)) p / (algebraMap (Polynomial F) (RatFunc F)) q) = (algebraMap (Polynomial F) (LaurentSeries F)) p / (algebraMap (Polynomial F) (LaurentSeries F)) q

def PowerSeries.idealX (K : Type u_2) [Field K] : IsDedekindDomain.HeightOneSpectrum (PowerSeries K)

The prime ideal (X) of K⟦X⟧, when K is a field, as a term of the HeightOneSpectrum.

theorem PowerSeries.intValuation_eq_of_coe {K : Type u_2} [Field K] (P : Polynomial K) : (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

@[simp]

theorem PowerSeries.intValuation_X {K : Type u_2} [Field K] : (idealX K).intValuation X = WithZero.exp (-1)

The integral valuation of the power series X : K⟦X⟧ equals (ofAdd -1) : ℤᵐ⁰.

theorem RatFunc.valuation_eq_LaurentSeries_valuation (K : Type u_2) [Field K] (P : RatFunc K) : (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K)) P = (IsDedekindDomain.HeightOneSpectrum.valuation (LaurentSeries K) (PowerSeries.idealX K)) ((algebraMap (RatFunc K) (LaurentSeries K)) P)

instance LaurentSeries.instValuedWithZeroMultiplicativeInt (K : Type u_2) [Field K] : Valued (LaurentSeries K) (WithZero (Multiplicative ℤ))

theorem LaurentSeries.valuation_def (K : Type u_2) [Field K] : Valued.v = IsDedekindDomain.HeightOneSpectrum.valuation (LaurentSeries K) (PowerSeries.idealX K)

@[simp]

theorem LaurentSeries.valuation_coe_ratFunc (K : Type u_2) [Field K] (f : RatFunc K) : Valued.v ((algebraMap (RatFunc K) (LaurentSeries K)) f) = Valued.v f

theorem LaurentSeries.valuation_X_pow (K : Type u_2) [Field K] (s : ℕ) : Valued.v ((HahnSeries.ofPowerSeries ℤ K) PowerSeries.X ^ s) = WithZero.exp (-↑s)

theorem LaurentSeries.valuation_single_zpow (K : Type u_2) [Field K] (s : ℤ) : Valued.v ((HahnSeries.single s) 1) = WithZero.exp (-s)

theorem LaurentSeries.coeff_zero_of_lt_intValuation (K : Type u_2) [Field K] {n d : ℕ} {f : PowerSeries K} (H : Valued.v ((HahnSeries.ofPowerSeries ℤ K) f) ≤ WithZero.exp (-↑d)) : n < d → (PowerSeries.coeff n) f = 0

theorem LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero (K : Type u_2) [Field K] {d : ℕ} (f : PowerSeries K) : Valued.v ((HahnSeries.ofPowerSeries ℤ K) f) ≤ WithZero.exp (-↑d) ↔ ∀ n < d, (PowerSeries.coeff n) f = 0

theorem LaurentSeries.coeff_zero_of_lt_valuation (K : Type u_2) [Field K] {n D : ℤ} {f : LaurentSeries K} (H : Valued.v f ≤ WithZero.exp (-D)) : n < D → f.coeff n = 0

theorem LaurentSeries.valuation_le_iff_coeff_lt_eq_zero (K : Type u_2) [Field K] {D : ℤ} {f : LaurentSeries K} : Valued.v f ≤ WithZero.exp (-D) ↔ ∀ n < D, f.coeff n = 0

theorem LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero (K : Type u_2) [Field K] {D : WithZero (Multiplicative ℤ)} (hD : D ≠ 0) {f : LaurentSeries K} : Valued.v f ≤ D ↔ ∀ n < -D.log, f.coeff n = 0

theorem LaurentSeries.eq_coeff_of_valuation_sub_lt (K : Type u_2) [Field K] {d n : ℤ} {f g : LaurentSeries K} (H : Valued.v (g - f) ≤ WithZero.exp (-d)) : n < d → g.coeff n = f.coeff n

theorem LaurentSeries.val_le_one_iff_eq_coe (K : Type u_2) [Field K] (f : LaurentSeries K) : Valued.v f ≤ 1 ↔ ∃ (F : PowerSeries K), (HahnSeries.ofPowerSeries ℤ K) F = f

theorem LaurentSeries.uniformContinuous_coeff {K : Type u_2} [Field K] {uK : UniformSpace K} (d : ℤ) : UniformContinuous fun (f : LaurentSeries K) => f.coeff d

def LaurentSeries.Cauchy.coeff {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) : ℤ → K

Since extracting coefficients is uniformly continuous, every Cauchy filter in K⸨X⸩ gives rise to a Cauchy filter in K for every d : ℤ, and such Cauchy filter in K converges to a principal filter

theorem LaurentSeries.Cauchy.coeff_tendsto {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) (D : ℤ) : Filter.Tendsto (fun (f : LaurentSeries K) => f.coeff D) ℱ (Filter.principal {coeff hℱ D})

theorem LaurentSeries.Cauchy.exists_lb_eventual_support {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) : ∃ (N : ℤ), ∀ᶠ (f : LaurentSeries K) in ℱ, ∀ n < N, f.coeff n = 0

theorem LaurentSeries.Cauchy.exists_lb_support {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) : ∃ (N : ℤ), ∀ n < N, coeff hℱ n = 0

theorem LaurentSeries.Cauchy.coeff_support_bddBelow {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) : BddBelow (Function.support (coeff hℱ))

def LaurentSeries.Cauchy.limit {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) : LaurentSeries K

To any Cauchy filter ℱ of K⸨X⸩, we can attach a laurent series that is the limit of the filter. Its d-th coefficient is defined as the limit of Cauchy.coeff hℱ d, which is again Cauchy but valued in the discrete space K. That sufficiently negative coefficients vanish follows from Cauchy.coeff_support_bddBelow

theorem LaurentSeries.Cauchy.exists_lb_coeff_ne {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) : ∃ (N : ℤ), ∀ᶠ (f : LaurentSeries K) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d

theorem LaurentSeries.Cauchy.coeff_eventually_equal {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) {D : ℤ} : ∀ᶠ (f : LaurentSeries K) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d

theorem LaurentSeries.Cauchy.eventually_mem_nhds {K : Type u_2} [Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) {U : Set (LaurentSeries K)} (hU : U ∈ nhds (limit hℱ)) : ∀ᶠ (f : LaurentSeries K) in ℱ, f ∈ U

instance LaurentSeries.instLaurentSeriesComplete {K : Type u_2} [Field K] : CompleteSpace (LaurentSeries K)

theorem LaurentSeries.exists_Polynomial_intValuation_lt {K : Type u_2} [Field K] (F : PowerSeries K) (η : (WithZero (Multiplicative ℤ))ˣ) : ∃ (P : Polynomial K), (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η

theorem LaurentSeries.exists_ratFunc_val_lt {K : Type u_2} [Field K] (f : LaurentSeries K) (γ : (WithZero (Multiplicative ℤ))ˣ) : ∃ (Q : RatFunc K), Valued.v (f - (algebraMap (RatFunc K) (LaurentSeries K)) Q) < ↑γ

For every Laurent series f and every γ : ℤᵐ⁰ one can find a rational function Q such that the X-adic valuation v satisfies v (f - Q) < γ.

theorem LaurentSeries.coe_range_dense {K : Type u_2} [Field K] : DenseRange ⇑(algebraMap (RatFunc K) (LaurentSeries K))

theorem LaurentSeries.exists_ratFunc_eq_v {K : Type u_2} [Field K] (x : LaurentSeries K) : ∃ (f : RatFunc K), Valued.v f = Valued.v x

theorem LaurentSeries.inducing_coe {K : Type u_2} [Field K] : IsUniformInducing ⇑(algebraMap (RatFunc K) (LaurentSeries K))

theorem LaurentSeries.continuous_coe {K : Type u_2} [Field K] : Continuous ⇑(algebraMap (RatFunc K) (LaurentSeries K))

@[reducible, inline]

abbrev LaurentSeries.ratfuncAdicComplPkg {K : Type u_2} [Field K] : AbstractCompletion.{u_2, u_2} (RatFunc K)

The X-adic completion as an abstract completion of RatFunc K

noncomputable def LaurentSeries.LaurentSeriesPkg (K : Type u_2) [Field K] : AbstractCompletion.{u_2, u_2} (RatFunc K)

Having established that the K⸨X⸩ is complete and contains RatFunc K as a dense subspace, it gives rise to an abstract completion of RatFunc K.

instance LaurentSeries.instTopologicalSpaceSpaceRatFuncLaurentSeriesPkg (K : Type u_2) [Field K] : TopologicalSpace (LaurentSeriesPkg K).space

@[simp]

theorem LaurentSeries.LaurentSeries_coe (K : Type u_2) [Field K] (x : RatFunc K) : (LaurentSeriesPkg K).coe x = (algebraMap (RatFunc K) (LaurentSeries K)) x

@[reducible, inline]

abbrev LaurentSeries.extensionAsRingHom (K : Type u_2) [Field K] (hf : Continuous ⇑(algebraMap (RatFunc K) (LaurentSeries K))) [CompleteSpace (LaurentSeries K)] [T0Space (LaurentSeries K)] : UniformSpace.Completion (RatFunc K) →+* LaurentSeries K

Reinterpret the extension of coe : RatFunc K → K⸨X⸩ as a ring homomorphism

@[reducible, inline]

abbrev LaurentSeries.RatFuncAdicCompl (K : Type u_2) [Field K] : Type u_2

An abbreviation for the X-adic completion of RatFunc K

instance LaurentSeries.instUniformSpaceRatFuncAdicCompl (K : Type u_2) [Field K] : UniformSpace (RatFuncAdicCompl K)

instance LaurentSeries.instUniformSpace (K : Type u_2) [Field K] : UniformSpace (LaurentSeries K)

@[reducible, inline]

abbrev LaurentSeries.comparePkg (K : Type u_2) [Field K] : RatFuncAdicCompl K ≃ᵤ LaurentSeries K

The uniform space isomorphism between two abstract completions of ratfunc K

theorem LaurentSeries.comparePkg_eq_extension (K : Type u_2) [Field K] (x : UniformSpace.Completion (RatFunc K)) : (comparePkg K).toFun x = (↑↑(extensionAsRingHom K ⋯)).toFun x

@[reducible, inline]

abbrev LaurentSeries.ratfuncAdicComplRingEquiv (K : Type u_2) [Field K] : RatFuncAdicCompl K ≃+* LaurentSeries K

The uniform space equivalence between two abstract completions of ratfunc K as a ring equivalence: this will be the inverse of the fundamental one.

@[reducible, inline]

abbrev LaurentSeries.LaurentSeriesRingEquiv (K : Type u_2) [Field K] : LaurentSeries K ≃+* RatFuncAdicCompl K

The uniform space equivalence between two abstract completions of ratfunc K as a ring equivalence: it goes from K⸨X⸩ to RatFuncAdicCompl K

@[simp]

theorem LaurentSeries.LaurentSeriesRingEquiv_def (K : Type u_2) [Field K] (f : PowerSeries K) : (LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) f) = (LaurentSeriesPkg K).compare ratfuncAdicComplPkg ((HahnSeries.ofPowerSeries ℤ K) f)

@[simp]

theorem LaurentSeries.ratfuncAdicComplRingEquiv_apply (K : Type u_2) [Field K] (x : RatFuncAdicCompl K) : (ratfuncAdicComplRingEquiv K) x = ratfuncAdicComplPkg.compare (LaurentSeriesPkg K) x

theorem LaurentSeries.coe_X_compare (K : Type u_2) [Field K] : (ratfuncAdicComplRingEquiv K) ↑RatFunc.X = (HahnSeries.ofPowerSeries ℤ K) PowerSeries.X

theorem LaurentSeries.algebraMap_apply (K : Type u_2) [Field K] (a : K) : (algebraMap K (LaurentSeries K)) a = HahnSeries.C a

instance LaurentSeries.instAlgebraRatFuncAdicCompl (K : Type u_2) [Field K] : Algebra K (RatFuncAdicCompl K)

def LaurentSeries.LaurentSeriesAlgEquiv (K : Type u_2) [Field K] : LaurentSeries K ≃ₐ[K] RatFuncAdicCompl K

The algebra equivalence between K⸨X⸩ and the X-adic completion of RatFunc X

theorem LaurentSeries.valuation_LaurentSeries_equal_extension (K : Type u_2) [Field K] : ⋯.extend ⇑Valued.v = ⇑Valued.v

theorem LaurentSeries.tendsto_valuation (K : Type u_2) [Field K] (a : IsDedekindDomain.HeightOneSpectrum.adicCompletion (RatFunc K) (Polynomial.idealX K)) : Filter.Tendsto (⇑Valued.v) (Filter.comap UniformSpace.Completion.coe' (nhds a)) (nhds (Valued.v a))

theorem LaurentSeries.valuation_compare (K : Type u_2) [Field K] (f : LaurentSeries K) : Valued.v ((LaurentSeriesPkg K).compare ratfuncAdicComplPkg f) = Valued.v f

@[reducible, inline]

abbrev LaurentSeries.powerSeries_as_subring (K : Type u_2) [Field K] : Subring (LaurentSeries K)

In order to compare K⟦X⟧ with the valuation subring in the X-adic completion of RatFunc K we consider its alias as a subring of K⸨X⸩.

@[reducible, inline]

abbrev LaurentSeries.powerSeriesEquivSubring (K : Type u_2) [Field K] : PowerSeries K ≃+* ↥(powerSeries_as_subring K)

The ring K⟦X⟧ is isomorphic to the subring powerSeries_as_subring K

theorem LaurentSeries.powerSeriesEquivSubring_apply (K : Type u_2) [Field K] (f : PowerSeries K) : (powerSeriesEquivSubring K) f = ⟨(HahnSeries.ofPowerSeries ℤ K) f, ⋯⟩

theorem LaurentSeries.powerSeriesEquivSubring_coe_apply (K : Type u_2) [Field K] (f : PowerSeries K) : ↑((powerSeriesEquivSubring K) f) = (HahnSeries.ofPowerSeries ℤ K) f

theorem LaurentSeries.mem_integers_of_powerSeries (K : Type u_2) [Field K] (F : PowerSeries K) : (LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) F) ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K)

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

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

@[reducible, inline]

abbrev LaurentSeries.powerSeriesRingEquiv (K : Type u_2) [Field K] : PowerSeries K ≃+* ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K))

The ring isomorphism between K⟦X⟧ and the unit ball inside the X-adic completion of RatFunc K.

theorem LaurentSeries.powerSeriesRingEquiv_coe_apply (K : Type u_2) [Field K] (f : PowerSeries K) : ↑((powerSeriesRingEquiv K) f) = (LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) f)

theorem LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring (K : Type u_2) [Field K] (f : PowerSeries K) : (LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) f) ∈ Valued.v.valuationSubring

theorem LaurentSeries.algebraMap_C_mem_adicCompletionIntegers (K : Type u_2) [Field K] (x : K) : ((LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K)

instance LaurentSeries.instAlgebraSubtypeAdicCompletionPolynomialRatFuncIdealXMemValuationSubringAdicCompletionIntegers (K : Type u_2) [Field K] : Algebra K ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K))

def LaurentSeries.powerSeriesAlgEquiv (K : Type u_2) [Field K] : PowerSeries K ≃ₐ[K] ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K))

The algebra isomorphism between K⟦X⟧ and the unit ball inside the X-adic completion of RatFunc K.