Theorems · Definition · commutative algebra

LaurentSeries.LaurentSeriesPkg

(K : Type u_2) → [inst : Field K] → AbstractCompletion.{u_2, u_2} (WithVal (RatFunc.polynomialValuationX K))

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

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

6 results in Mathlib

Foundations

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

Assumes

Field