residueFieldOfPowerSeries — Mathlib

English

The residue field of the local ring k[[X]] is canonically isomorphic to k.

Русский

Остаточное поле локального кольца k[[X]] канонически изоморфно k.

LaTeX

$$k[[X]]\text{ residue field } \cong k$$

Lean4

/-- The ring isomorphism between the residue field of the ring of power series valued in a field `K`
and `K` itself. -/
def residueFieldOfPowerSeries : ResidueField k⟦X⟧ ≃+* k :=
  (Ideal.quotEquivOfEq (ker_coeff_eq_max_ideal).symm).trans (RingHom.quotientKerEquivOfSurjective constantCoeff_surj)

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