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
@[instance]
def polynomial.semimodule {R : Type u} [semiring R] {S : Type u_1} [semiring S] [semimodule S R] :

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

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

monomial s a is the monomial a * X^s

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

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

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

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

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

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

X is the polynomial variable (aka indeterminant).

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

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

theorem polynomial.X_pow_mul {R : Type u} [semiring R] {p : polynomial R} {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) :

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

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

Equations
@[simp]
theorem polynomial.coeff_mk {R : Type u} [semiring R] (s : finset ) (f : → R) (h : ∀ (a : ), a s f a 0) :

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] :

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

theorem polynomial.coeff_X {R : Type u} {n : } [semiring R] :
polynomial.X.coeff n = ite (1 = n) 1 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

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) :
a 0((polynomial.monomial n) a).support = {n}

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

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

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

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

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

Equations
@[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

@[instance]

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

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

Equations