Theorems · Definition · commutative algebra

LaurentSeries.extensionAsRingHom

(K : Type u_2) →
  [inst : Field K] →
    Continuous
        ⇑((algebraMap (RatFunc K) (LaurentSeries K)).comp (WithVal.equiv (RatFunc.polynomialValuationX K)).toRingHom) →
      [CompleteSpace (LaurentSeries K)] →
        [T0Space (LaurentSeries K)] →
          UniformSpace.Completion (WithVal (RatFunc.polynomialValuationX K)) →+* LaurentSeries K

Reinterpret the extension of coe : WithVal ((idealX K).valuation _) → K⸨X⸩ as a ring homomorphism

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldCompleteSpaceT0Space