# mathlib3documentation

ring_theory.polynomial.cyclotomic.eval

# Evaluating cyclotomic polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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} [comm_ring R] {p : } [hn : fact (nat.prime p)] :
= p
@[simp]
theorem polynomial.eval₂_one_cyclotomic_prime {R : Type u_1} {S : Type u_2} [comm_ring R] [semiring S] (f : R →+* S) {p : } [fact (nat.prime p)] :
= p
@[simp]
theorem polynomial.eval_one_cyclotomic_prime_pow {R : Type u_1} [comm_ring R] {p : } (k : ) [hn : fact (nat.prime p)] :
(polynomial.cyclotomic (p ^ (k + 1)) R) = p
@[simp]
theorem polynomial.eval₂_one_cyclotomic_prime_pow {R : Type u_1} {S : Type u_2} [comm_ring R] [semiring S] (f : R →+* S) {p : } (k : ) [fact (nat.prime p)] :
(polynomial.cyclotomic (p ^ (k + 1)) R) = p
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 < x 0 < R)) (1 x 0 R))
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 : }, (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_nat_abs_cyclotomic_eval {n q : } (hn' : 1 < n) (hq : q 1) :
(q - 1) ^ n.totient <
theorem polynomial.sub_one_lt_nat_abs_cyclotomic_eval {n q : } (hn' : 1 < n) (hq : q 1) :
q - 1 <