one_le_convexBodyLT'Factor — Mathlib

English

Let K be a field equipped with a NumberField structure. Then the LT' factor is bounded below by 1: convexBodyLT'Factor K ≥ 1.

Русский

Пусть K – поле с дополнением NumberField. Тогда коэффициент convexBodyLT'Factor не меньше единицы: convexBodyLT'Factor K ≥ 1.

LaTeX

$$$1 \\le convexBodyLT'(K)$$$

Lean4

theorem one_le_convexBodyLT'Factor : 1 ≤ convexBodyLT'Factor K :=
  one_le_mul (one_le_pow₀ one_le_two) (one_le_pow₀ (one_le_two.trans Real.two_le_pi))

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