sub_one_pow_totient_le_cyclotomic_eval

English

For q > 1, for every n, (q − 1)^{totient(n)} ≤ cyclotomic(n, Real).eval(q).

Русский

Для q > 1 и любого n верно (q − 1)^{φ(n)} ≤ cyclotomic(n, Real).eval(q).

LaTeX

$$(q - 1) ^ totient(n) ≤ (cyclotomic(n, Real)).eval(q)$$

Lean4

theorem sub_one_pow_totient_le_cyclotomic_eval {q : ℝ} (hq' : 1 < q) :
    ∀ n, (q - 1) ^ totient n ≤ (cyclotomic n ℝ).eval q
  | 0 => by simp only [totient_zero, _root_.pow_zero, cyclotomic_zero, eval_one, le_refl]
  | 1 => by simp only [totient_one, pow_one, cyclotomic_one, eval_sub, eval_X, eval_one, le_refl]
  | _ + 2 => (sub_one_pow_totient_lt_cyclotomic_eval le_add_self hq').le

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