cyclotomic_eval_le_add_one_pow_totient

English

For q > 1, for every n, cyclotomic(n, Real).eval(q) ≤ (q + 1)^{totient(n)}, with base cases n = 0,1,2 handled separately.

Русский

Для q > 1 и любого n выполняется неравенство cyclotomic(n, Real).eval(q) ≤ (q+1)^{φ(n)} с учётом базовых случаев n = 0,1,2.

LaTeX

$$∀ n, cyclotomic(n, Real).eval(q) ≤ (q + 1)^{totient(n)}$$

Lean4

theorem cyclotomic_eval_le_add_one_pow_totient {q : ℝ} (hq' : 1 < q) :
    ∀ n, (cyclotomic n ℝ).eval q ≤ (q + 1) ^ totient n
  | 0 => by simp
  | 1 => by simp [add_assoc, zero_le_one]
  | 2 => by simp
  | _ + 3 => (cyclotomic_eval_lt_add_one_pow_totient le_add_self hq').le

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