instFintypeElemIdealPrimesOver

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

URI: https://scilib.ai/kg/mathlib#instFintypeElemIdealPrimesOver

English

The ncard (cardinality) of primes over p is nonzero; there exists at least one prime over p.

Русский

Кардинальность множества primesOver p не нулевая; существует по меньшей мере один простой над p.

LaTeX

$$p.primesOver B .ncard ≠ 0$$

Lean4

noncomputable instance : Fintype (p.primesOver B) :=
  Set.Finite.fintype (primesOver_finite p B)

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

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

Разделы

Аффилиация

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