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)
if2 < n
.
@[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
@[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
@[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
@[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
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)
theorem
polynomial.eval_one_cyclotomic_not_prime_pow
{R : Type u_1}
[comm_ring R]
{n : ℕ}
(h : ∀ {p : ℕ}, nat.prime p → ∀ (k : ℕ), p ^ k ≠ n) :
polynomial.eval 1 (polynomial.cyclotomic n R) = 1