Theory of univariate polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The theorems include formulas for computing coefficients, such as
coeff_add, coeff_sum, coeff_mul
@[simp]
theorem
polynomial.coeff_smul
{R : Type u}
{S : Type v}
[semiring R]
[smul_zero_class S R]
(r : S)
(p : polynomial R)
(n : ℕ) :
theorem
polynomial.support_smul
{R : Type u}
{S : Type v}
[semiring R]
[monoid S]
[distrib_mul_action S R]
(r : S)
(p : polynomial R) :
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 A →ₗ[R] M
polynomial.sum as a linear map.
Equations
- polynomial.lsum f = {to_fun := λ (p : polynomial A), p.sum (λ (n : ℕ) (r : A), ⇑(f n) r), map_add' := _, map_smul' := _}
The nth coefficient, as a linear map.
Equations
- polynomial.lcoeff R n = {to_fun := λ (p : polynomial R), p.coeff n, map_add' := _, map_smul' := _}
@[simp]
theorem
polynomial.lcoeff_apply
{R : Type u}
[semiring R]
(n : ℕ)
(f : polynomial R) :
⇑(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.
@[simp]
theorem
polynomial.constant_coeff_apply
{R : Type u}
[semiring R]
(p : polynomial R) :
⇑polynomial.constant_coeff p = p.coeff 0
constant_coeff p returns the constant term of the polynomial p,
defined as coeff p 0. This is a ring homomorphism.
Equations
- polynomial.constant_coeff = {to_fun := λ (p : polynomial R), p.coeff 0, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
theorem
polynomial.is_unit_C
{R : Type u}
[semiring R]
{x : R} :
is_unit (⇑polynomial.C x) ↔ is_unit x
theorem
polynomial.coeff_mul_X_zero
{R : Type u}
[semiring R]
(p : polynomial R) :
(p * polynomial.X).coeff 0 = 0
theorem
polynomial.coeff_X_mul_zero
{R : Type u}
[semiring R]
(p : polynomial R) :
(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
@[simp]
theorem
polynomial.C_mul'
{R : Type u}
[semiring R]
(a : R)
(f : polynomial R) :
⇑polynomial.C a * f = a • f
@[simp]
@[simp]
theorem
polynomial.coeff_X_pow_self
{R : Type u}
[semiring R]
(n : ℕ) :
(polynomial.X ^ n).coeff n = 1
theorem
polynomial.support_binomial
{R : Type u}
[semiring R]
{k m : ℕ}
(hkm : k ≠ m)
{x y : R}
(hx : x ≠ 0)
(hy : y ≠ 0) :
(⇑polynomial.C x * polynomial.X ^ k + ⇑polynomial.C y * polynomial.X ^ m).support = {k, m}
theorem
polynomial.support_trinomial
{R : Type u}
[semiring R]
{k m n : ℕ}
(hkm : k < m)
(hmn : m < n)
{x y z : R}
(hx : x ≠ 0)
(hy : y ≠ 0)
(hz : z ≠ 0) :
(⇑polynomial.C x * polynomial.X ^ k + ⇑polynomial.C y * polynomial.X ^ m + ⇑polynomial.C z * polynomial.X ^ n).support = {k, m, n}
theorem
polynomial.card_support_binomial
{R : Type u}
[semiring R]
{k m : ℕ}
(h : k ≠ m)
{x y : R}
(hx : x ≠ 0)
(hy : y ≠ 0) :
(⇑polynomial.C x * polynomial.X ^ k + ⇑polynomial.C y * polynomial.X ^ m).support.card = 2
theorem
polynomial.card_support_trinomial
{R : Type u}
[semiring R]
{k m n : ℕ}
(hkm : k < m)
(hmn : m < n)
{x y z : R}
(hx : x ≠ 0)
(hy : y ≠ 0)
(hz : z ≠ 0) :
(⇑polynomial.C x * polynomial.X ^ k + ⇑polynomial.C y * polynomial.X ^ m + ⇑polynomial.C z * polynomial.X ^ n).support.card = 3
@[simp]
@[simp]
@[simp]
@[simp]
theorem
polynomial.coeff_mul_monomial
{R : Type u}
[semiring R]
(p : polynomial R)
(n d : ℕ)
(r : R) :
theorem
polynomial.coeff_monomial_mul
{R : Type u}
[semiring R]
(p : polynomial R)
(n d : ℕ)
(r : R) :
theorem
polynomial.coeff_mul_monomial_zero
{R : Type u}
[semiring R]
(p : polynomial R)
(d : ℕ)
(r : R) :
theorem
polynomial.coeff_monomial_zero_mul
{R : Type u}
[semiring R]
(p : polynomial R)
(d : ℕ)
(r : R) :
theorem
polynomial.mul_X_pow_eq_zero
{R : Type u}
[semiring R]
{p : polynomial R}
{n : ℕ}
(H : p * polynomial.X ^ n = 0) :
p = 0
theorem
polynomial.mul_X_pow_injective
{R : Type u}
[semiring R]
(n : ℕ) :
function.injective (λ (P : polynomial R), polynomial.X ^ n * P)
theorem
polynomial.mul_X_injective
{R : Type u}
[semiring R] :
function.injective (λ (P : polynomial R), polynomial.X * P)
theorem
polynomial.smul_eq_C_mul
{R : Type u}
[semiring R]
{p : polynomial R}
(a : R) :
a • p = ⇑polynomial.C a * p
theorem
polynomial.update_eq_add_sub_coeff
{R : Type u_1}
[ring R]
(p : polynomial R)
(n : ℕ)
(a : R) :
p.update n a = p + ⇑polynomial.C (a - p.coeff n) * polynomial.X ^ n
@[protected, instance]