LaurentSeriesRingEquiv_mem_valuationSubring

English

For any f in PowerSeries K, the image under LaurentSeriesRingEquiv lies in the valuation subring of the completion.

Русский

Для любого f из PowerSeries K образ через LaurentSeriesRingEquiv лежит в ценностном подкольстве завершения.

LaTeX

$$$\\mathrm{LaurentSeriesRingEquiv}\\;K\\;f \\in \\mathrm{Valued.v}.\\mathrm{valuationSubring}$$$

Lean4

theorem LaurentSeriesRingEquiv_mem_valuationSubring (f : K⟦X⟧) :
    LaurentSeriesRingEquiv K f ∈ Valued.v.valuationSubring :=
  by
  simp only [Valuation.mem_valuationSubring_iff]
  rw [LaurentSeriesRingEquiv_def, valuation_compare, val_le_one_iff_eq_coe]
  use f

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