instIsFractionRingPowerSeries — Mathlib

English

If R is a field, PowerSeries R embeds into LaurentSeries R as a fraction ring: LaurentSeries R is the fraction field of PowerSeries R.

Русский

Если R — поле, PowerSeries R внедряется в LaurentSeries R как дробное поле: LaurentSeries R является полем дробей PowerSeries R.

LaTeX

$$$\text{IsFractionRing }(\text{PowerSeries } K)\; (\text{LaurentSeries } K)$$$

Lean4

instance {K : Type*} [Field K] : IsFractionRing K⟦X⟧ K⸨X⸩ :=
  IsLocalization.of_le (Submonoid.powers (PowerSeries.X : K⟦X⟧)) _
    (powers_le_nonZeroDivisors_of_noZeroDivisors PowerSeries.X_ne_zero) fun _ hf =>
    isUnit_of_mem_nonZeroDivisors <| map_mem_nonZeroDivisors _ HahnSeries.ofPowerSeries_injective hf

Похожие утверждения