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} [CommRing R] {p : ℕ} [hn : Fact (Nat.Prime p)] : eval 1 (cyclotomic p R) = ↑p

theorem Polynomial.eval₂_one_cyclotomic_prime {R : Type u_1} {S : Type u_2} [CommRing R] [Semiring S] (f : R →+* S) {p : ℕ} [Fact (Nat.Prime p)] : eval₂ f 1 (cyclotomic p R) = ↑p

@[simp]

theorem Polynomial.eval_one_cyclotomic_prime_pow {R : Type u_1} [CommRing R] {p : ℕ} (k : ℕ) [hn : Fact (Nat.Prime p)] : eval 1 (cyclotomic (p ^ (k + 1)) R) = ↑p

theorem Polynomial.eval₂_one_cyclotomic_prime_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Semiring S] (f : R →+* S) {p : ℕ} (k : ℕ) [Fact (Nat.Prime p)] : eval₂ f 1 (cyclotomic (p ^ (k + 1)) R) = ↑p

theorem Polynomial.cyclotomic_pos {n : ℕ} (hn : 2 < n) {R : Type u_1} [LinearOrderedCommRing R] (x : R) : 0 < eval x (cyclotomic n R)

theorem Polynomial.cyclotomic_pos_and_nonneg (n : ℕ) {R : Type u_1} [LinearOrderedCommRing R] (x : R) : (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R))

theorem Polynomial.cyclotomic_pos' (n : ℕ) {R : Type u_1} [LinearOrderedCommRing R] {x : R} (hx : 1 < x) : 0 < eval x (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.

theorem Polynomial.cyclotomic_nonneg (n : ℕ) {R : Type u_1} [LinearOrderedCommRing R] {x : R} (hx : 1 ≤ x) : 0 ≤ eval x (cyclotomic n R)

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 : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n) : eval 1 (cyclotomic n R) = 1

theorem Polynomial.sub_one_pow_totient_lt_cyclotomic_eval {n : ℕ} {q : ℝ} (hn' : 2 ≤ n) (hq' : 1 < q) : (q - 1) ^ n.totient < eval q (cyclotomic n ℝ)

theorem Polynomial.sub_one_pow_totient_le_cyclotomic_eval {q : ℝ} (hq' : 1 < q) (n : ℕ) : (q - 1) ^ n.totient ≤ eval q (cyclotomic n ℝ)

theorem Polynomial.cyclotomic_eval_lt_add_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤ n) (hq' : 1 < q) : eval q (cyclotomic n ℝ) < (q + 1) ^ n.totient

theorem Polynomial.cyclotomic_eval_le_add_one_pow_totient {q : ℝ} (hq' : 1 < q) (n : ℕ) : eval q (cyclotomic 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 < (eval (↑q) (cyclotomic n ℤ)).natAbs

theorem Polynomial.sub_one_lt_natAbs_cyclotomic_eval {n q : ℕ} (hn' : 1 < n) (hq : q ≠ 1) : q - 1 < (eval (↑q) (cyclotomic n ℤ)).natAbs