minimalPrimes_isPrime

Mathlib.RingTheory.Ideal.MinimalPrime.Basic

URI: https://scilib.ai/kg/mathlib#Ideal.minimalPrimes_isPrime

English

If p is a minimal prime over I, then p is a prime ideal.

Русский

Если p является минимальным простым над I, то p — простый идеал.

LaTeX

$$$\forall p\; (p \in I.minimalPrimes) \Rightarrow p.isPrime$$$

Lean4

theorem minimalPrimes_isPrime {p : Ideal R} (h : p ∈ I.minimalPrimes) : p.IsPrime :=
  h.1.1

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

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

Разделы

Аффилиация

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