ker_residue

Mathlib.RingTheory.LocalRing.ResidueField.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalRing.ker_residue

English

The kernel of the residue map from R to its residue field is exactly the maximal ideal.

Русский

Ядро отображения остатка R → R/m совпадает с максимальным идеалом m.

LaTeX

$$$\\operatorname{ker}(\\mathrm{residue}_R) = \\mathfrak m_R$$$

Lean4

theorem ker_residue : RingHom.ker (residue R) = maximalIdeal R :=
  Ideal.mk_ker

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru