Theorems · Theorem · commutative algebra

LaurentSeries.exists_ratFunc_val_lt

∀ {K : Type u_2} [inst : Field K] (f : LaurentSeries K) (γ : (WithZero (Multiplicative ℤ))ˣ),
  ∃ Q, 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) < γ.

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field