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

monomial s a is the monomial a * X^s

Equations
@[simp]
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) :
@[simp]
theorem polynomial.monomial_pow {R : Type u} [semiring R] (n : ) (r : 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) :
theorem polynomial.support_add {R : Type u} [semiring R] {p q : polynomial 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) :
@[simp]
theorem polynomial.monomial_mul_X {R : Type u} [semiring R] (n : ) (r : R) :
@[simp]
theorem polynomial.monomial_mul_X_pow {R : Type u} [semiring R] (n : ) (r : R) (k : ) :
@[simp]
theorem polynomial.X_mul_monomial {R : Type u} [semiring R] (n : ) (r : R) :
@[simp]
theorem polynomial.X_pow_mul_monomial {R : Type u} [semiring R] (k n : ) (r : 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
@[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] :
@[simp]
theorem polynomial.coeff_monomial_succ {R : Type u} {a : R} {n : } [semiring R] :
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) :
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) :
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] (H : 1 = 0) :
theorem polynomial.support_X {R : Type u} [semiring R] (H : ¬1 = 0) :
theorem polynomial.monomial_left_inj {R : Type u_1} [semiring R] {a : R} (ha : a 0) {i j : } :
theorem polynomial.nat_cast_mul {R : Type u_1} [semiring R] (n : ) (p : polynomial R) :
(n) * p = n p
@[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
@[simp]
theorem polynomial.monomial_neg {R : Type u} [ring R] (n : ) (a : R) :
@[simp]
theorem polynomial.support_neg {R : Type u} [ring R] {p : polynomial R} :
@[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