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.
• Notation to refer to polynomial R, as R[X] or R[t].

Implementation #

Polynomials are defined using add_monoid_algebra R ℕ, where R is a semiring. The variable X commutes with every polynomial p: lemma X_mul proves the identity X * p =p * X. The relationship toadd_monoid_algebra R ℕis through a structure to make polynomials irreducible from the point of view of the kernel. Most operations are irreducible since Lean can not compute anyway withadd_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.

Conversions to and from add_monoid_algebra #

Since polynomial R is not defeq to add_monoid_algebra R ℕ, but instead is a structure wrapping it, we have to copy across all the arithmetic operators manually, along with the lemmas about how they unfold around polynomial.of_finsupp and polynomial.to_finsupp.