residue — Mathlib

English

The canonical quotient map from a local ring R to its residue field κ(R) is the natural projection R → R/𝔪.

Русский

Каноническое отображение к остаточному полю задаётся естественным образом как проекция R → R/м.

LaTeX

$$$\operatorname{residue}: R \to \operatorname{ResidueField} R$ is the quotient map by the maximal ideal.$$

Lean4

/-- The quotient map from a local ring to its residue field. -/
def residue : R →+* ResidueField R :=
  Ideal.Quotient.mk _

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