instIsLocalRing — Mathlib

English

Multivariate power series over a local ring form a local ring.

Русский

Многомерные формальные ряды над локальным кольцом образуют локальное кольцо.

LaTeX

$$$ IsLocalRing (MvPowerSeries σ R) $$$

Lean4

/-- Multivariate formal power series over a local ring form a local ring. -/
instance [IsLocalRing R] : IsLocalRing (MvPowerSeries σ R) :=
  IsLocalRing.of_isUnit_or_isUnit_one_sub_self <| by
    intro φ
    obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ) <;> [left; right] <;>
      · refine isUnit_of_mul_eq_one _ _ (mul_invOfUnit _ u ?_)
        simpa using h.symm

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