setOf_isPrime_finite

Mathlib.RingTheory.Artinian.Module

URI: https://scilib.ai/kg/mathlib#IsArtinianRing.setOf_isPrime_finite

English

The set of all prime ideals is finite in an Artinian ring.

Русский

Множество всех простых идеалов конечное в артиновом кольце.

LaTeX

$$$\{ I : \text{Ideal}(R) \mid I.\text{IsPrime} \}.\text{Finite}$$$

Lean4

theorem setOf_isPrime_finite : {I : Ideal R | I.IsPrime}.Finite := by
  simpa only [isPrime_iff_isMaximal] using setOf_isMaximal_finite R

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

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

Разделы

Аффилиация

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