finite_residueField_of_compactSpace

Mathlib.Topology.Algebra.Ring.Compact

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

English

The residue field at the unique maximal ideal of R is finite.

Русский

Остаточное поле при единственной максимальной идеале кольца R конечно.

LaTeX

$$$ Finite( R / maximalIdeal(R) ) $$$

Lean4

instance finite_residueField_of_compactSpace : Finite (ResidueField R) :=
  inferInstanceAs (Finite (R ⧸ _))

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

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

Разделы

Аффилиация

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