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.

source

@[simp]

theorem polynomial.eval_one_cyclotomic_prime {R : Type u_1} [comm_ring R] {p : ℕ} [hn : fact (nat.prime p)] :

polynomial.eval 1 (polynomial.cyclotomic p R) = ↑p

source

@[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)] :

polynomial.eval₂ f 1 (polynomial.cyclotomic p R) = ↑p

source

@[simp]

theorem polynomial.eval_one_cyclotomic_prime_pow {R : Type u_1} [comm_ring R] {p : ℕ} (k : ℕ) [hn : fact (nat.prime p)] :

polynomial.eval 1 (polynomial.cyclotomic (p ^ (k + 1)) R) = ↑p

source

@[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.eval₂ f 1 (polynomial.cyclotomic (p ^ (k + 1)) R) = ↑p

source

theorem polynomial.cyclotomic_pos {n : ℕ} (hn : 2 < n) {R : Type u_1} [linear_ordered_comm_ring R] (x : R) :

0 < polynomial.eval x (polynomial.cyclotomic n R)

source

theorem polynomial.cyclotomic_pos_and_nonneg (n : ℕ) {R : Type u_1} [linear_ordered_comm_ring R] (x : R) :

(1 < x → 0 < polynomial.eval x (polynomial.cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ polynomial.eval x (polynomial.cyclotomic n R))

source

theorem polynomial.cyclotomic_pos' (n : ℕ) {R : Type u_1} [linear_ordered_comm_ring R] {x : R} (hx : 1 < x) :

0 < polynomial.eval x (polynomial.cyclotomic n R)

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.

source

theorem polynomial.cyclotomic_nonneg (n : ℕ) {R : Type u_1} [linear_ordered_comm_ring R] {x : R} (hx : 1 ≤ x) :

0 ≤ polynomial.eval x (polynomial.cyclotomic n R)

Cyclotomic polynomials are always nonnegative on inputs one or more.

source

theorem polynomial.eval_one_cyclotomic_not_prime_pow {R : Type u_1} [ring R] {n : ℕ} (h : ∀ {p : ℕ}, nat.prime p → ∀ (k : ℕ), p ^ k ≠ n) :

polynomial.eval 1 (polynomial.cyclotomic n R) = 1

source

theorem polynomial.sub_one_pow_totient_lt_cyclotomic_eval {n : ℕ} {q : ℝ} (hn' : 2 ≤ n) (hq' : 1 < q) :

(q - 1) ^ n.totient < polynomial.eval q (polynomial.cyclotomic n ℝ)

source

theorem polynomial.sub_one_pow_totient_le_cyclotomic_eval {q : ℝ} (hq' : 1 < q) (n : ℕ) :

(q - 1) ^ n.totient ≤ polynomial.eval q (polynomial.cyclotomic n ℝ)

source

theorem polynomial.cyclotomic_eval_lt_add_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤ n) (hq' : 1 < q) :

polynomial.eval q (polynomial.cyclotomic n ℝ) < (q + 1) ^ n.totient

source

theorem polynomial.cyclotomic_eval_le_add_one_pow_totient {q : ℝ} (hq' : 1 < q) (n : ℕ) :

polynomial.eval q (polynomial.cyclotomic n ℝ) ≤ (q + 1) ^ n.totient

source

theorem polynomial.sub_one_pow_totient_lt_nat_abs_cyclotomic_eval {n q : ℕ} (hn' : 1 < n) (hq : q ≠ 1) :

(q - 1) ^ n.totient < (polynomial.eval ↑q (polynomial.cyclotomic n ℤ)).nat_abs

source

theorem polynomial.sub_one_lt_nat_abs_cyclotomic_eval {n q : ℕ} (hn' : 1 < n) (hq : q ≠ 1) :

q - 1 < (polynomial.eval ↑q (polynomial.cyclotomic n ℤ)).nat_abs