le_maximalIdeal_of_isPrime — Mathlib

English

Let R be a commutative local ring and p a prime ideal of R. Then p is contained in the maximal ideal of R.

Русский

Пусть R — коммутативное локальное кольцо и p — простой идеал R. Тогда p содержится в максимальном идеале R.

LaTeX

$$$ p \subseteq \mathfrak{m} \quad\text{where } \mathfrak{m} = \operatorname{maximalIdeal}(R). $$$

Lean4

theorem le_maximalIdeal_of_isPrime (p : Ideal R) [hp : p.IsPrime] : p ≤ maximalIdeal R :=
  le_maximalIdeal hp.ne_top

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