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.
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]
Equations
@[instance]
Equations
@[instance]
@[instance]
monomial s a is the monomial a * X^s
Equations
- polynomial.monomial n a = finsupp.single n a
@[simp]
theorem
polynomial.monomial_zero_right
{R : Type u}
[semiring R]
(n : ℕ) :
polynomial.monomial n 0 = 0
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)
X is the polynomial variable (aka indeterminant).
Equations
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
coeff p n is the coefficient of X^n in p
theorem
polynomial.coeff_monomial
{R : Type u}
{a : R}
{m n : ℕ}
[semiring R] :
(polynomial.monomial n a).coeff m = ite (n = m) a 0
theorem
polynomial.coeff_single
{R : Type u}
{a : R}
{m n : ℕ}
[semiring R] :
polynomial.coeff (finsupp.single n a) m = ite (n = m) a 0
This lemma is needed for occasions when we break through the abstraction from
polynomial to finsupp; ideally it wouldn't be necessary at all.
@[simp]
theorem
polynomial.coeff_X
{R : Type u}
{n : ℕ}
[semiring R] :
polynomial.X.coeff n = ite (1 = n) 1 0
@[ext]
theorem
polynomial.eq_zero_of_eq_zero
{R : Type u}
[semiring R]
(h : 0 = 1)
(p : polynomial R) :
p = 0
@[instance]
Equations
@[simp]
@[instance]
@[instance]
@[instance]
Equations
@[instance]
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))}