height_eq_primeHeight

Mathlib.RingTheory.Ideal.Height

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

← MathLib Explorer

English

If I is a prime ideal, then height(I) = primeHeight(I).

Русский

Если I — простой идеал, то height(I) = primeHeight(I).

LaTeX

$$$I.height = I.primeHeight$$$

Lean4

/-- For a prime ideal, its height equals its prime height. -/
theorem height_eq_primeHeight [I.IsPrime] : I.height = I.primeHeight :=
  by
  unfold height primeHeight
  simp_rw [Ideal.minimalPrimes_eq_subsingleton_self]
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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