Theory of univariate polynomials #

This file defines polynomial R, the type of univariate polynomials over the semiring R, builds a semiring structure on it, and gives basic definitions that are expanded in other files in this directory.

Main definitions #

• monomial n a is the polynomial a X^n. Note that monomial n is defined as an R-linear map.
• C a is the constant polynomial a. Note that C is defined as a ring homomorphism.
• X is the polynomial X, i.e., monomial 1 1.
• p.sum f is ∑ n in p.support, f n (p.coeff n), i.e., one sums the values of functions applied to coefficients of the polynomial p.
• p.erase n is the polynomial p in which one removes the c X^n term.

There are often two natural variants of lemmas involving sums, depending on whether one acts on the polynomials, or on the function. The naming convention is that one adds index when acting on the polynomials. For instance,

• sum_add_index states that (p + q).sum f = p.sum f + q.sum f;
• sum_add states that p.sum (λ n x, f n x + g n x) = p.sum f + p.sum g.

Implementation #

Polynomials are defined using add_monoid_algebra R ℕ, where R is a commutative semiring, but through a structure to make them irreducible from the point of view of the kernel. Most operations are irreducible since Lean can not compute anyway with add_monoid_algebra. There are two exceptions that we make semireducible:

• The zero polynomial, so that its coefficients are definitionally equal to 0.
• The scalar action, to permit typeclass search to unfold it to resolve potential instance diamonds.

The raw implementation of the equivalence between polynomial R and add_monoid_algebra R ℕ is done through of_finsupp and to_finsupp (or, equivalently, rcases p when p is a polynomial gives an element q of add_monoid_algebra R ℕ, and conversely ⟨q⟩ gives back p). The equivalence is also registered as a ring equiv in polynomial.to_finsupp_iso. These should in general not be used once the basic API for polynomials is constructed.