English
For n and q in natural numbers, if n ≥ 2 and q ≠ 1, then (q − 1)^{totient(n)} < |cyclotomic(n, Z).eval(q)|.
Русский
Для n ≥ 2 и q ≠ 1 верно (q − 1)^{φ(n)} < |cyclotomic(n, Z).eval(q)|.
LaTeX
$$(q - 1) ^ totient(n) < ((cyclotomic n Z).eval q).natAbs$$
Lean4
theorem sub_one_pow_totient_lt_natAbs_cyclotomic_eval {n : ℕ} {q : ℕ} (hn' : 1 < n) (hq : q ≠ 1) :
(q - 1) ^ totient n < ((cyclotomic n ℤ).eval ↑q).natAbs :=
by
rcases hq.lt_or_gt.imp_left Nat.lt_one_iff.mp with (rfl | hq')
· rw [zero_tsub, zero_pow (Nat.totient_pos.2 (pos_of_gt hn')).ne', pos_iff_ne_zero, Int.natAbs_ne_zero, Nat.cast_zero,
← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hn']
exact one_ne_zero
rw [← @Nat.cast_lt ℝ, Nat.cast_pow, Nat.cast_sub hq'.le, Nat.cast_one, Int.cast_natAbs]
refine (sub_one_pow_totient_lt_cyclotomic_eval hn' (Nat.one_lt_cast.2 hq')).trans_le ?_
convert (cyclotomic.eval_apply (q : ℤ) n (algebraMap ℤ ℝ)).trans_le (le_abs_self _)
simp
