exists_prime

Mathlib.RingTheory.DiscreteValuationRing.Basic

URI: https://scilib.ai/kg/mathlib#IsDiscreteValuationRing.exists_prime

English

There exists a prime element in a DVR.

Русский

Существует простой элемент в DVR.

LaTeX

$$$\exists \varpi, Prime \varpi$$$

Lean4

/-- Uniformizers exist in a DVR. -/
theorem exists_prime : ∃ ϖ : R, Prime ϖ :=
  (exists_irreducible R).imp fun _ => irreducible_iff_prime.1

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

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

Разделы

Аффилиация

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