sub_one_lt_natAbs_cyclotomic_eval

English

For n ≥ 2 and q ≠ 1, q − 1 < |cyclotomic(n, Z).eval(q)|.

Русский

Для n ≥ 2 и q ≠ 1 верно: q − 1 < |cyclotomic(n, Z).eval(q)|.

LaTeX

$$q - 1 < ((cyclotomic n Z).eval ↑q).natAbs$$

Lean4

theorem sub_one_lt_natAbs_cyclotomic_eval {n : ℕ} {q : ℕ} (hn' : 1 < n) (hq : q ≠ 1) :
    q - 1 < ((cyclotomic n ℤ).eval ↑q).natAbs :=
  calc
    q - 1 ≤ (q - 1) ^ totient n := Nat.le_self_pow (Nat.totient_pos.2 <| pos_of_gt hn').ne' _
    _ < ((cyclotomic n ℤ).eval ↑q).natAbs := sub_one_pow_totient_lt_natAbs_cyclotomic_eval hn' hq

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