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.

theorem Polynomial.eval_one_cyclotomic_prime {R : Type u_1} [CommRing R] {p : Nat} [hn : Fact (Nat.Prime p)] : Eq (eval 1 (cyclotomic p R)) p.cast

theorem Polynomial.eval₂_one_cyclotomic_prime {R : Type u_1} {S : Type u_2} [CommRing R] [Semiring S] (f : RingHom R S) {p : Nat} [Fact (Nat.Prime p)] : Eq (eval₂ f 1 (cyclotomic p R)) p.cast

theorem Polynomial.eval_one_cyclotomic_prime_pow {R : Type u_1} [CommRing R] {p : Nat} (k : Nat) [hn : Fact (Nat.Prime p)] : Eq (eval 1 (cyclotomic (HPow.hPow p (HAdd.hAdd k 1)) R)) p.cast

theorem Polynomial.eval₂_one_cyclotomic_prime_pow {R : Type u_1} {S : Type u_2} [CommRing R] [Semiring S] (f : RingHom R S) {p : Nat} (k : Nat) [Fact (Nat.Prime p)] : Eq (eval₂ f 1 (cyclotomic (HPow.hPow p (HAdd.hAdd k 1)) R)) p.cast

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

theorem Polynomial.cyclotomic_pos_and_nonneg (n : Nat) {R : Type u_1} [LinearOrderedCommRing R] (x : R) : And (LT.lt 1 x → LT.lt 0 (eval x (cyclotomic n R))) (LE.le 1 x → LE.le 0 (eval x (cyclotomic n R)))

theorem Polynomial.cyclotomic_pos' (n : Nat) {R : Type u_1} [LinearOrderedCommRing R] {x : R} (hx : LT.lt 1 x) : LT.lt 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 : Nat) {R : Type u_1} [LinearOrderedCommRing R] {x : R} (hx : LE.le 1 x) : LE.le 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 : Nat} (h : ∀ {p : Nat}, Nat.Prime p → ∀ (k : Nat), Ne (HPow.hPow p k) n) : Eq (eval 1 (cyclotomic n R)) 1

theorem Polynomial.sub_one_pow_totient_lt_cyclotomic_eval {n : Nat} {q : Real} (hn' : LE.le 2 n) (hq' : LT.lt 1 q) : LT.lt (HPow.hPow (HSub.hSub q 1) n.totient) (eval q (cyclotomic n Real))

theorem Polynomial.sub_one_pow_totient_le_cyclotomic_eval {q : Real} (hq' : LT.lt 1 q) (n : Nat) : LE.le (HPow.hPow (HSub.hSub q 1) n.totient) (eval q (cyclotomic n Real))

theorem Polynomial.cyclotomic_eval_lt_add_one_pow_totient {n : Nat} {q : Real} (hn' : LE.le 3 n) (hq' : LT.lt 1 q) : LT.lt (eval q (cyclotomic n Real)) (HPow.hPow (HAdd.hAdd q 1) n.totient)

theorem Polynomial.cyclotomic_eval_le_add_one_pow_totient {q : Real} (hq' : LT.lt 1 q) (n : Nat) : LE.le (eval q (cyclotomic n Real)) (HPow.hPow (HAdd.hAdd q 1) n.totient)

theorem Polynomial.sub_one_pow_totient_lt_natAbs_cyclotomic_eval {n q : Nat} (hn' : LT.lt 1 n) (hq : Ne q 1) : LT.lt (HPow.hPow (HSub.hSub q 1) n.totient) (eval q.cast (cyclotomic n Int)).natAbs

theorem Polynomial.sub_one_lt_natAbs_cyclotomic_eval {n q : Nat} (hn' : LT.lt 1 n) (hq : Ne q 1) : LT.lt (HSub.hSub q 1) (eval q.cast (cyclotomic n Int)).natAbs