Theory of univariate polynomials #
The theorems include formulas for computing coefficients, such as
coeff_add, coeff_sum, coeff_mul
theorem
polynomial.support_smul
{R : Type u}
{S : Type v}
[semiring R]
[monoid S]
[distrib_mul_action S R]
(r : S)
(p : R[X]) :
def
polynomial.lsum
{R : Type u_1}
{A : Type u_2}
{M : Type u_3}
[semiring R]
[semiring A]
[add_comm_monoid M]
[module R A]
[module R M]
(f : ℕ → (A →ₗ[R] M)) :
polynomial.sum as a linear map.
@[simp]
theorem
polynomial.lcoeff_apply
{R : Type u}
[semiring R]
(n : ℕ)
(f : R[X]) :
⇑(polynomial.lcoeff R n) f = f.coeff n
Decomposes the coefficient of the product p * q as a sum
over nat.antidiagonal. A version which sums over range (n + 1) can be obtained
by using finset.nat.sum_antidiagonal_eq_sum_range_succ.
theorem
polynomial.coeff_mul_X_zero
{R : Type u}
[semiring R]
(p : R[X]) :
(p * polynomial.X).coeff 0 = 0
theorem
polynomial.coeff_X_mul_zero
{R : Type u}
[semiring R]
(p : R[X]) :
(polynomial.X * p).coeff 0 = 0
theorem
polynomial.coeff_C_mul_X_pow
{R : Type u}
[semiring R]
(x : R)
(k n : ℕ) :
((⇑polynomial.C x) * polynomial.X ^ k).coeff n = ite (n = k) x 0
theorem
polynomial.coeff_C_mul_X
{R : Type u}
[semiring R]
(x : R)
(n : ℕ) :
((⇑polynomial.C x) * polynomial.X).coeff n = ite (n = 1) x 0
theorem
polynomial.C_mul'
{R : Type u}
[semiring R]
(a : R)
(f : R[X]) :
(⇑polynomial.C a) * f = a • f
@[simp]
theorem
polynomial.coeff_X_pow_self
{R : Type u}
[semiring R]
(n : ℕ) :
(polynomial.X ^ n).coeff n = 1
theorem
polynomial.mul_X_pow_eq_zero
{R : Type u}
[semiring R]
{p : R[X]}
{n : ℕ}
(H : p * polynomial.X ^ n = 0) :
p = 0
theorem
polynomial.mul_X_pow_injective
{R : Type u}
[semiring R]
(n : ℕ) :
function.injective (λ (P : R[X]), (polynomial.X ^ n) * P)
theorem
polynomial.mul_X_injective
{R : Type u}
[semiring R] :
function.injective (λ (P : R[X]), polynomial.X * P)
theorem
polynomial.C_mul_X_pow_eq_monomial
{R : Type u}
[semiring R]
(c : R)
(n : ℕ) :
(⇑polynomial.C c) * polynomial.X ^ n = ⇑(polynomial.monomial n) c
theorem
polynomial.support_mul_X_pow
{R : Type u}
[semiring R]
(c : R)
(n : ℕ)
(H : c ≠ 0) :
((⇑polynomial.C c) * polynomial.X ^ n).support = {n}
theorem
polynomial.support_C_mul_X_pow'
{R : Type u}
[semiring R]
{c : R}
{n : ℕ} :
((⇑polynomial.C c) * polynomial.X ^ n).support ⊆ {n}
theorem
polynomial.smul_eq_C_mul
{R : Type u}
[semiring R]
{p : R[X]}
(a : R) :
a • p = (⇑polynomial.C a) * p
theorem
polynomial.update_eq_add_sub_coeff
{R : Type u_1}
[ring R]
(p : R[X])
(n : ℕ)
(a : R) :
p.update n a = p + (⇑polynomial.C (a - p.coeff n)) * polynomial.X ^ n