Theory of univariate polynomials #
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]
[monoid S]
[distrib_mul_action 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' := _}
@[simp]
theorem
polynomial.lsum_apply
{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))
(p : polynomial A) :
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
theorem
polynomial.coeff_sum
{R : Type u}
{S : Type v}
[semiring R]
{p : polynomial R}
[semiring S]
(n : ℕ)
(f : ℕ → R → polynomial S) :
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.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.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.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]