mathlib documentation

data.polynomial.basic

Theory of univariate polynomials #

Polynomials are represented as add_monoid_algebra R ℕ, where R is a commutative semiring. In this file, we define polynomial, provide basic instances, and prove an ext lemma.

def polynomial (R : Type u_1) [semiring R] :

Type u_1

polynomial R is the type of univariate polynomials over R.

Polynomials should be seen as (semi-)rings with the additional constructor X. The embedding from R is called C.

Equations

polynomial R = add_monoid_algebra R ℕ

@[instance]

def polynomial.inhabited {R : Type u} [semiring R] :

inhabited (polynomial R)

Equations

polynomial.inhabited = add_monoid_algebra.inhabited R ℕ

@[instance]

def polynomial.semiring {R : Type u} [semiring R] :

semiring (polynomial R)

Equations

polynomial.semiring = add_monoid_algebra.semiring

@[instance]

def polynomial.semimodule {R : Type u} [semiring R] {S : Type u_1} [semiring S] [semimodule S R] :

semimodule S (polynomial R)

Equations

polynomial.semimodule = add_monoid_algebra.semimodule

@[instance]

def polynomial.smul_comm_class {R : Type u} [semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [semiring S₁] [semiring S₂] [semimodule S₁ R] [semimodule S₂ R] [smul_comm_class S₁ S₂ R] :

smul_comm_class S₁ S₂ (polynomial R)

@[instance]

def polynomial.is_scalar_tower {R : Type u} [semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [has_scalar S₁ S₂] [semiring S₁] [semiring S₂] [semimodule S₁ R] [semimodule S₂ R] [is_scalar_tower S₁ S₂ R] :

is_scalar_tower S₁ S₂ (polynomial R)

@[instance]

def polynomial.unique {R : Type u} [semiring R] [subsingleton R] :

unique (polynomial R)

Equations

polynomial.unique = add_monoid_algebra.unique

def polynomial.support {R : Type u} [semiring R] (p : polynomial R) :

The set of all n such that X^n has a non-zero coefficient.

Equations

p.support = p.support

@[simp]

theorem polynomial.support_zero {R : Type u} [semiring R] :

0.support = ∅

@[simp]

theorem polynomial.support_eq_empty {R : Type u} [semiring R] {p : polynomial R} :

p.support = ∅ ↔ p = 0

theorem polynomial.card_support_eq_zero {R : Type u} [semiring R] {p : polynomial R} :

p.support.card = 0 ↔ p = 0

def polynomial.monomial {R : Type u} [semiring R] (n : ℕ) :

R →ₗ[R] polynomial R

monomial s a is the monomial a * X^s

Equations

polynomial.monomial n = finsupp.lsingle n

@[simp]

theorem polynomial.monomial_zero_right {R : Type u} [semiring R] (n : ℕ) :

⇑(polynomial.monomial n) 0 = 0

theorem polynomial.monomial_zero_one {R : Type u} [semiring R] :

⇑(polynomial.monomial 0) 1 = 1

theorem polynomial.monomial_def {R : Type u} [semiring R] (n : ℕ) (a : R) :

⇑(polynomial.monomial n) a = finsupp.single n a

theorem polynomial.monomial_add {R : Type u} [semiring R] (n : ℕ) (r s : R) :

⇑(polynomial.monomial n) (r + s) = ⇑(polynomial.monomial n) r + ⇑(polynomial.monomial n) s

theorem polynomial.monomial_mul_monomial {R : Type u} [semiring R] (n m : ℕ) (r s : R) :

(⇑(polynomial.monomial n) r) * ⇑(polynomial.monomial m) s = ⇑(polynomial.monomial (n + m)) (r * s)

@[simp]

theorem polynomial.monomial_pow {R : Type u} [semiring R] (n : ℕ) (r : R) (k : ℕ) :

⇑(polynomial.monomial n) r ^ k = ⇑(polynomial.monomial (n * k)) (r ^ k)

theorem polynomial.smul_monomial {R : Type u} [semiring R] {S : Type u_1} [semiring S] [semimodule S R] (a : S) (n : ℕ) (b : R) :

a • ⇑(polynomial.monomial n) b = ⇑(polynomial.monomial n) (a • b)

theorem polynomial.support_add {R : Type u} [semiring R] {p q : polynomial R} :

(p + q).support ⊆ p.support ∪ q.support

def polynomial.X {R : Type u} [semiring R] :

X is the polynomial variable (aka indeterminant).

Equations

polynomial.X = ⇑(polynomial.monomial 1) 1

theorem polynomial.monomial_one_one_eq_X {R : Type u} [semiring R] :

⇑(polynomial.monomial 1) 1 = polynomial.X

theorem polynomial.monomial_one_right_eq_X_pow (n : ℕ) :

⇑(polynomial.monomial n) 1 = polynomial.X ^ n

theorem polynomial.X_mul {R : Type u} [semiring R] {p : polynomial R} :

polynomial.X * p = p * polynomial.X

X commutes with everything, even when the coefficients are noncommutative.

theorem polynomial.X_pow_mul {R : Type u} [semiring R] {p : polynomial R} {n : ℕ} :

(polynomial.X ^ n) * p = p * polynomial.X ^ n

theorem polynomial.X_pow_mul_assoc {R : Type u} [semiring R] {p q : polynomial R} {n : ℕ} :

(p * polynomial.X ^ n) * q = (p * q) * polynomial.X ^ n

theorem polynomial.commute_X {R : Type u} [semiring R] (p : polynomial R) :

commute polynomial.X p

@[simp]

theorem polynomial.monomial_mul_X {R : Type u} [semiring R] (n : ℕ) (r : R) :

(⇑(polynomial.monomial n) r) * polynomial.X = ⇑(polynomial.monomial (n + 1)) r

@[simp]

theorem polynomial.monomial_mul_X_pow {R : Type u} [semiring R] (n : ℕ) (r : R) (k : ℕ) :

(⇑(polynomial.monomial n) r) * polynomial.X ^ k = ⇑(polynomial.monomial (n + k)) r

@[simp]

theorem polynomial.X_mul_monomial {R : Type u} [semiring R] (n : ℕ) (r : R) :

polynomial.X * ⇑(polynomial.monomial n) r = ⇑(polynomial.monomial (n + 1)) r

@[simp]

theorem polynomial.X_pow_mul_monomial {R : Type u} [semiring R] (k n : ℕ) (r : R) :

(polynomial.X ^ k) * ⇑(polynomial.monomial n) r = ⇑(polynomial.monomial (n + k)) r

def polynomial.coeff {R : Type u} [semiring R] (p : polynomial R) :

ℕ → R

coeff p n is the coefficient of X^n in p

Equations

p.coeff = ⇑p

@[simp]

theorem polynomial.coeff_mk {R : Type u} [semiring R] (s : finset ℕ) (f : ℕ → R) (h : ∀ (a : ℕ), a ∈ s ↔ f a ≠ 0) :

polynomial.coeff {support := s, to_fun := f, mem_support_to_fun := h} = f

theorem polynomial.coeff_monomial {R : Type u} {a : R} {m n : ℕ} [semiring R] :

(⇑(polynomial.monomial n) a).coeff m = ite (n = m) a 0

@[simp]

theorem polynomial.coeff_zero {R : Type u} [semiring R] (n : ℕ) :

0.coeff n = 0

@[simp]

theorem polynomial.coeff_one_zero {R : Type u} [semiring R] :

1.coeff 0 = 1

@[simp]

theorem polynomial.coeff_X_one {R : Type u} [semiring R] :

polynomial.X.coeff 1 = 1

@[simp]

theorem polynomial.coeff_X_zero {R : Type u} [semiring R] :

polynomial.X.coeff 0 = 0

@[simp]

theorem polynomial.coeff_monomial_succ {R : Type u} {a : R} {n : ℕ} [semiring R] :

(⇑(polynomial.monomial (n + 1)) a).coeff 0 = 0

theorem polynomial.coeff_X {R : Type u} {n : ℕ} [semiring R] :

polynomial.X.coeff n = ite (1 = n) 1 0

theorem polynomial.coeff_X_of_ne_one {R : Type u} [semiring R] {n : ℕ} (hn : n ≠ 1) :

polynomial.X.coeff n = 0

theorem polynomial.ext_iff {R : Type u} [semiring R] {p q : polynomial R} :

p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n

@[ext]

theorem polynomial.ext {R : Type u} [semiring R] {p q : polynomial R} :

(∀ (n : ℕ), p.coeff n = q.coeff n) → p = q

@[ext]

theorem polynomial.add_hom_ext' {R : Type u} [semiring R] {M : Type u_1} [add_monoid M] {f g : polynomial R →+ M} (h : ∀ (n : ℕ), f.comp (polynomial.monomial n).to_add_monoid_hom = g.comp (polynomial.monomial n).to_add_monoid_hom) :

f = g

theorem polynomial.add_hom_ext {R : Type u} [semiring R] {M : Type u_1} [add_monoid M] {f g : polynomial R →+ M} (h : ∀ (n : ℕ) (a : R), ⇑f (⇑(polynomial.monomial n) a) = ⇑g (⇑(polynomial.monomial n) a)) :

f = g

@[ext]

theorem polynomial.lhom_ext' {R : Type u} [semiring R] {M : Type u_1} [add_comm_monoid M] [semimodule R M] {f g : polynomial R →ₗ[R] M} (h : ∀ (n : ℕ), f.comp (polynomial.monomial n) = g.comp (polynomial.monomial n)) :

f = g

theorem polynomial.eq_zero_of_eq_zero {R : Type u} [semiring R] (h : 0 = 1) (p : polynomial R) :

p = 0

theorem polynomial.support_monomial {R : Type u} [semiring R] (n : ℕ) (a : R) (H : a ≠ 0) :

(⇑(polynomial.monomial n) a).support = {n}

theorem polynomial.support_monomial' {R : Type u} [semiring R] (n : ℕ) (a : R) :

(⇑(polynomial.monomial n) a).support ⊆ {n}

theorem polynomial.X_pow_eq_monomial {R : Type u} [semiring R] (n : ℕ) :

polynomial.X ^ n = ⇑(polynomial.monomial n) 1

theorem polynomial.support_X_pow {R : Type u} [semiring R] (H : ¬1 = 0) (n : ℕ) :

(polynomial.X ^ n).support = {n}

theorem polynomial.support_X_empty {R : Type u} [semiring R] (H : 1 = 0) :

polynomial.X.support = ∅

theorem polynomial.support_X {R : Type u} [semiring R] (H : ¬1 = 0) :

polynomial.X.support = {1}

theorem polynomial.monomial_left_inj {R : Type u_1} [semiring R] {a : R} (ha : a ≠ 0) {i j : ℕ} :

⇑(polynomial.monomial i) a = ⇑(polynomial.monomial j) a ↔ i = j

theorem polynomial.nat_cast_mul {R : Type u_1} [semiring R] (n : ℕ) (p : polynomial R) :

(↑n) * p = n • p

@[instance]

def polynomial.comm_semiring {R : Type u} [comm_semiring R] :

comm_semiring (polynomial R)

Equations

polynomial.comm_semiring = add_monoid_algebra.comm_semiring

@[instance]

def polynomial.ring {R : Type u} [ring R] :

ring (polynomial R)

Equations

polynomial.ring = add_monoid_algebra.ring

@[simp]

theorem polynomial.coeff_neg {R : Type u} [ring R] (p : polynomial R) (n : ℕ) :

(-p).coeff n = -p.coeff n

@[simp]

theorem polynomial.coeff_sub {R : Type u} [ring R] (p q : polynomial R) (n : ℕ) :

(p - q).coeff n = p.coeff n - q.coeff n

@[simp]

theorem polynomial.monomial_neg {R : Type u} [ring R] (n : ℕ) (a : R) :

⇑(polynomial.monomial n) (-a) = -⇑(polynomial.monomial n) a

@[simp]

theorem polynomial.support_neg {R : Type u} [ring R] {p : polynomial R} :

(-p).support = p.support

@[instance]

def polynomial.comm_ring {R : Type u} [comm_ring R] :

comm_ring (polynomial R)

Equations

polynomial.comm_ring = add_monoid_algebra.comm_ring

@[instance]

def polynomial.nontrivial {R : Type u} [semiring R] [nontrivial R] :

nontrivial (polynomial R)

theorem polynomial.X_ne_zero {R : Type u} [semiring R] [nontrivial R] :

polynomial.X ≠ 0

@[instance]

def polynomial.has_repr {R : Type u} [semiring R] [has_repr R] :

has_repr (polynomial R)

Equations

polynomial.has_repr = {repr := λ (p : polynomial R), ite (p = 0) "0" (list.foldr (λ (n : ℕ) (a : string), a ++ ite (a = "") "" " + " ++ ite (n = 0) ("C (" ++ repr (p.coeff n) ++ ")") (ite (n = 1) (ite (p.coeff n = 1) "X" ("C (" ++ repr (p.coeff n) ++ ") * X")) (ite (p.coeff n = 1) ("X ^ " ++ repr n) ("C (" ++ repr (p.coeff n) ++ ") * X ^ " ++ repr n)))) "" (finset.sort has_le.le p.support))}