Polynomial.eval_one_cyclotomic_prime_pow
theorem Polynomial.eval_one_cyclotomic_prime_pow :
∀ {R : Type u_1} [inst : CommRing R] {p : ℕ} (k : ℕ) [hn : Fact p.Prime],
Polynomial.eval 1 (Polynomial.cyclotomic (p ^ (k + 1)) R) = ↑p
This theorem states that for any commutative ring `R`, any natural number `k`, and any prime number `p`, the evaluation of the `(p^(k+1))`-th cyclotomic polynomial at `1` is equal to `p`. In other words, if you plug in `1` into the `(p^(k+1))`-th cyclotomic polynomial, you get the prime number `p` as a result, no matter what commutative ring the polynomial's coefficients are taken from.
More concisely: For any prime number p and natural number k, the value of the p^(k+1)-th cyclotomic polynomial evaluated at 1 is equal to p.
|
Polynomial.cyclotomic_pos'
theorem Polynomial.cyclotomic_pos' :
∀ (n : ℕ) {R : Type u_1} [inst : LinearOrderedCommRing R] {x : R},
1 < x → 0 < Polynomial.eval x (Polynomial.cyclotomic n R)
This theorem states that for any natural number `n` and any element `x` from a linearly ordered commutative ring `R`, if `x` is greater than one, then the evaluation of the `n`-th cyclotomic polynomial with coefficients in `R` at `x` is positive. In other words, cyclotomic polynomials are always positive when evaluated at inputs larger than one. This is a generalization of the `cyclotomic_pos` theorem where the condition on positivity is placed on the input to the polynomial rather than the index of the cyclotomic polynomial.
More concisely: For any natural number `n` and any element `x` in a commutative ring with identity greater than 1, the `n`-th cyclotomic polynomial evaluated at `x` is a positive element in the ring.
|
Polynomial.cyclotomic_nonneg
theorem Polynomial.cyclotomic_nonneg :
∀ (n : ℕ) {R : Type u_1} [inst : LinearOrderedCommRing R] {x : R},
1 ≤ x → 0 ≤ Polynomial.eval x (Polynomial.cyclotomic n R)
The theorem `Polynomial.cyclotomic_nonneg` states that for any natural number `n` and any type `R` that is a linear ordered commutative ring, the `n`-th cyclotomic polynomial with coefficients in `R`, when evaluated at any `x` from `R` that is greater than or equal to one, is always nonnegative. In other words, if `x` is a value in a certain type of number system (linear ordered commutative ring) and `x` is one or more, then putting `x` into the `n`-th cyclotomic polynomial will always result in a value that is zero or positive.
More concisely: For any natural number `n` and any linear ordered commutative ring `R`, the `n`-th cyclotomic polynomial with coefficients in `R` evaluates to a nonnegative value for all `x` in `R` greater than or equal to one.
|