Theorems · Theorem · commutative algebra

LaurentSeries.Cauchy.coeff_eventually_equal

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

Given a Cauchy filter ℱ in the Laurent Series and a bound D, for almost all series in the filter the coefficients below D coincide with Cauchy.coeff hℱ.

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field