bound_aux — Mathlib

English

For n,d with d ≠ 0 and n ≥ 2, (d^{n-2})/n ≤ rothNumberNat((2d−1)^n).

Русский

При d ≠ 0 и n ≥ 2 верно (d^{n-2})/n ≤ rothNumberNat((2d−1)^n).

LaTeX

$$$ \\frac{d^{\\,n-2}}{n} \\leq \\operatorname{rothNumberNat}((2d-1)^n) $$$

Lean4

theorem bound_aux (hd : d ≠ 0) (hn : 2 ≤ n) : (d ^ (n - 2 :) / n : ℝ) ≤ rothNumberNat ((2 * d - 1) ^ n) :=
  by
  convert bound_aux' n d using 1
  rw [cast_mul, cast_pow, mul_comm, ← div_div, pow_sub₀ _ _ hn, ← div_eq_mul_inv, cast_pow]
  rwa [cast_ne_zero]

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