Documentation

Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Evaluating cyclotomic polynomials #

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

Main definitions #

@[simp]
theorem Polynomial.eval_one_cyclotomic_prime_pow {R : Type u_1} [CommRing R] {p : } (k : ) [hn : Fact (Nat.Prime 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)] :
theorem Polynomial.cyclotomic_pos {n : } (hn : 2 < n) {R : Type u_1} [LinearOrderedCommRing R] (x : R) :
theorem Polynomial.cyclotomic_pos' (n : ) {R : Type u_1} [LinearOrderedCommRing R] {x : R} (hx : 1 < x) :

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.

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) :
theorem Polynomial.sub_one_pow_totient_lt_cyclotomic_eval {n : } {q : } (hn' : 2 n) (hq' : 1 < q) :
theorem Polynomial.cyclotomic_eval_lt_add_one_pow_totient {n : } {q : } (hn' : 3 n) (hq' : 1 < q) :
theorem Polynomial.sub_one_pow_totient_lt_natAbs_cyclotomic_eval {n : } {q : } (hn' : 1 < n) (hq : q 1) :
(q - 1) ^ n.totient < (Polynomial.eval (↑q) (Polynomial.cyclotomic n )).natAbs
theorem Polynomial.sub_one_lt_natAbs_cyclotomic_eval {n : } {q : } (hn' : 1 < n) (hq : q 1) :
q - 1 < (Polynomial.eval (↑q) (Polynomial.cyclotomic n )).natAbs