one_le_primesOver_ncard

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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

English

The inequality 1 ≤ (primesOver p B).ncard follows from the nonzero cardinality result.

Русский

Неравенство 1 ≤ ncard(primesOver p B) следует из не нулевой кардинальности.

LaTeX

$$1 ≤ (primesOver p B).ncard$$

Lean4

theorem one_le_primesOver_ncard : 1 ≤ (primesOver p B).ncard :=
  Nat.one_le_iff_ne_zero.mpr (primesOver_ncard_ne_zero p B)

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

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

Разделы

Аффилиация

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