equivPrimesOver_apply

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply

← MathLib Explorer

English

For a maximal prime p in A, the set of primes over p in B is finite.

Русский

Для максимального простого p в A множество простых над p в B конечно.

LaTeX

$$primesOver p B is finite$$

Lean4

@[simp]
theorem equivPrimesOver_apply (hp : p ≠ 0) (v : { v : HeightOneSpectrum B // v.asIdeal ∣ map (algebraMap A B) p }) :
    equivPrimesOver B hp v = v.1.asIdeal :=
  rfl

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

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

Разделы

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

Аффилиация

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