convexBodySumFactor_ne_zero

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.convexBodySumFactor_ne_zero

← MathLib Explorer

English

The quantity convexBodySumFactor K is strictly positive (nonzero).

Русский

Число convexBodySumFactor K строго положительно.

LaTeX

$$convexBodySumFactor K ≠ 0$$

Lean4

theorem convexBodySumFactor_ne_zero : convexBodySumFactor K ≠ 0 :=
  by
  refine div_ne_zero ?_ <| Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
  exact mul_ne_zero (pow_ne_zero _ two_ne_zero) (pow_ne_zero _ (div_ne_zero NNReal.pi_ne_zero two_ne_zero))

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

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

Разделы

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

Аффилиация

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