# Evaluating cyclotomic polynomials #

This file states some results about evaluating cyclotomic polynomials in various different ways.

## Main definitions #

• Polynomial.eval(₂)_one_cyclotomic_prime(_pow): eval 1 (cyclotomic p^k R) = p.
• Polynomial.eval_one_cyclotomic_not_prime_pow: Otherwise, eval 1 (cyclotomic n R) = 1.
• Polynomial.cyclotomic_pos : ∀ x, 0 < eval x (cyclotomic n R) if 2 < n.
@[simp]
theorem Polynomial.eval_one_cyclotomic_prime {R : Type u_1} [] {p : } [hn : Fact p.Prime] :
= p
theorem Polynomial.eval₂_one_cyclotomic_prime {R : Type u_1} {S : Type u_2} [] [] (f : R →+* S) {p : } [Fact p.Prime] :
= p
@[simp]
theorem Polynomial.eval_one_cyclotomic_prime_pow {R : Type u_1} [] {p : } (k : ) [hn : Fact p.Prime] :
theorem Polynomial.eval₂_one_cyclotomic_prime_pow {R : Type u_1} {S : Type u_2} [] [] (f : R →+* S) {p : } (k : ) [Fact p.Prime] :
theorem Polynomial.cyclotomic_pos {n : } (hn : 2 < n) {R : Type u_1} (x : R) :
0 <
theorem Polynomial.cyclotomic_pos_and_nonneg (n : ) {R : Type u_1} (x : R) :
(1 < x0 < ) (1 x0 )
theorem Polynomial.cyclotomic_pos' (n : ) {R : Type u_1} {x : R} (hx : 1 < x) :
0 <

Cyclotomic polynomials are always positive on inputs larger than one. Similar to cyclotomic_pos but with the condition on the input rather than index of the cyclotomic polynomial.

theorem Polynomial.cyclotomic_nonneg (n : ) {R : Type u_1} {x : R} (hx : 1 x) :
0

Cyclotomic polynomials are always nonnegative on inputs one or more.

theorem Polynomial.eval_one_cyclotomic_not_prime_pow {R : Type u_1} [Ring R] {n : } (h : ∀ {p : }, p.Prime∀ (k : ), p ^ k n) :
= 1
theorem Polynomial.sub_one_pow_totient_lt_cyclotomic_eval {n : } {q : } (hn' : 2 n) (hq' : 1 < q) :
(q - 1) ^ n.totient <
theorem Polynomial.sub_one_pow_totient_le_cyclotomic_eval {q : } (hq' : 1 < q) (n : ) :
(q - 1) ^ n.totient
theorem Polynomial.cyclotomic_eval_lt_add_one_pow_totient {n : } {q : } (hn' : 3 n) (hq' : 1 < q) :
< (q + 1) ^ n.totient
theorem Polynomial.cyclotomic_eval_le_add_one_pow_totient {q : } (hq' : 1 < q) (n : ) :
(q + 1) ^ n.totient
theorem Polynomial.sub_one_pow_totient_lt_natAbs_cyclotomic_eval {n : } {q : } (hn' : 1 < n) (hq : q 1) :
(q - 1) ^ n.totient < ().natAbs
theorem Polynomial.sub_one_lt_natAbs_cyclotomic_eval {n : } {q : } (hn' : 1 < n) (hq : q 1) :
q - 1 < ().natAbs