Theorems · Theorem · commutative algebra

LaurentSeries.LaurentSeriesRingEquiv_def

∀ (K : Type u_2) [inst : Field K] (f : PowerSeries K),
  (LaurentSeries.LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) f) =
    {
      toCompletion :=
        (LaurentSeries.LaurentSeriesPkg K).compare LaurentSeries.ratfuncAdicComplPkg
          ((HahnSeries.ofPowerSeries ℤ K) f) }

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

0 results in Mathlib

Foundations

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

Assumes

Field