mathlib3 documentation

ring_theory.polynomial.cyclotomic.eval

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 #

@[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)] :
@[simp]
theorem polynomial.eval_one_cyclotomic_prime_pow {R : Type u_1} [comm_ring R] {p : } (k : ) [hn : fact (nat.prime 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)] :
theorem polynomial.cyclotomic_pos {n : } (hn : 2 < n) {R : Type u_1} [linear_ordered_comm_ring R] (x : R) :
theorem polynomial.cyclotomic_pos' (n : ) {R : Type u_1} [linear_ordered_comm_ring 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.

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

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) :