field

Mathlib.RingTheory.LocalRing.ResidueField.Defs

URI: https://scilib.ai/kg/mathlib#IsLocalRing.ResidueField.field

English

For a local ring R, its residue field R/m is a field, where m is the maximal ideal of R.

Русский

Для локального кольца R его остаточное поле R/m является полем, где m — максимальная идеал.

LaTeX

$$$\text{IsLocalRing}(R) \Rightarrow \text{Field}(\operatorname{ResidueField} R)$$$

Lean4

noncomputable instance field : Field (ResidueField R) :=
  Ideal.Quotient.field (maximalIdeal R)

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

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

Разделы

Аффилиация

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