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]
def
polynomial.semimodule
{R : Type u}
[semiring R]
{S : Type u_1}
[semiring S]
[semimodule S R] :
semimodule S (polynomial R)
@[instance]
Equations
monomial s a is the monomial a * X^s
Equations
theorem
polynomial.monomial_zero_right
{R : Type u}
[semiring R]
(n : ℕ) :
⇑(polynomial.monomial n) 0 = 0
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)
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)
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_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
@[ext]
@[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}
@[instance]
@[instance]
Equations
@[simp]
@[instance]
@[instance]
@[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))}