16.1. The polynomial ring
The type of univariate polynomials with coefficients in a semiring R is Polynomial.
To say "let f be a polynomial with coefficients in R", write:
variable (f : Polynomial R)
The notation R[X] for the polynomial ring over R is also available,
but it is scoped in the Polynomial namespace, so you have to open the scope to use it:
open scoped Polynomial
variable (g : R[X])
In what follows we work over an arbitrary semiring unless stated otherwise.
It is common to open the entire Polynomial namespace,
so that the names Polynomial.C, Polynomial.X, Polynomial.monomial,
Polynomial.eval, Polynomial.natDegree and Polynomial.degree
(and many others) can be written without the Polynomial prefix.
16.1.1. Constants and the indeterminate
The constant polynomials are the image of the coefficient semiring R
in R[X], embedded via the ring homomorphism Polynomial.C:
#check (Polynomial.C r : R[X])
The indeterminate of the polynomial ring is Polynomial.X:
#check (Polynomial.X : R[X])
Once the Polynomial namespace is open, you can write a polynomial as a Lean expression in C and X:
open Polynomial
#check (C r + C 2 * X ^ 2 + X ^ 3 : R[X])
16.1.2. Monomials
There is a dedicated constructor Polynomial.monomial for a single term,
taking the degree and the coefficient:
#check (monomial 3 r : R[X])
The identity Polynomial.C_mul_X_pow_eq_monomial translates between the two:
example : monomial 3 r = C r * X ^ 3 := R:Type u_1inst✝:Semiring Rr:Rn:ℕ⊢ (monomial 3) r = C r * X ^ 3
All goals completed! 🐙
Note that (monomial n : R →ₗ[R] R[X]) is itself an R-linear map
sending a coefficient to the corresponding monomial of degree n,
rather than a plain function of two arguments.
This is occasionally relevant when applying lemmas about linear maps to it.
In practice, concrete polynomials are usually written as sums of terms of the form
(C r * X ^ n : R[X]), rather than as (monomial n r : R[X]):
the C/X form composes naturally under +, * and ^,
and most arithmetic and coefficient lemmas are phrased against it.
The Polynomial.monomial form is most useful when you want to manipulate
a single term abstractly, for instance to use its linearity in the coefficient.
16.1.3. Coefficients
The coefficient of degree n of a polynomial p is Polynomial.coeff,
written p.coeff n:
example : R := p.coeff n
The basic identities for C, X and monomial are Polynomial.coeff_C,
Polynomial.coeff_X and Polynomial.coeff_monomial.
Two polynomials are equal iff all of their coefficients agree,
via Polynomial.coeff_inj and the extensionality lemma Polynomial.ext.
Coefficients of polynomials built from C, X and ring operations
can be computed term-by-term using Polynomial.coeff_add,
Polynomial.coeff_C_mul, Polynomial.coeff_X_pow
(together with Polynomial.coeff_C for constants).
For instance, the coefficients of C r + C 2 * X ^ 2 + X ^ 3 are
r, 0, 2, 1, then 0 from degree 4 on:
example (r : R) :
(C r + C 2 * X ^ 2 + X ^ 3 : R[X]).coeff 0 = r := R:Type u_1inst✝:Semiring Rp:R[X]n:ℕr:R⊢ (C r + C 2 * X ^ 2 + X ^ 3).coeff 0 = r
All goals completed! 🐙
example (r : R) :
(C r + C 2 * X ^ 2 + X ^ 3 : R[X]).coeff 2 = 2 := R:Type u_1inst✝:Semiring Rp:R[X]n:ℕr:R⊢ (C r + C 2 * X ^ 2 + X ^ 3).coeff 2 = 2
All goals completed! 🐙
example (r : R) :
(C r + C 2 * X ^ 2 + X ^ 3 : R[X]).coeff 3 = 1 := R:Type u_1inst✝:Semiring Rp:R[X]n:ℕr:R⊢ (C r + C 2 * X ^ 2 + X ^ 3).coeff 3 = 1
All goals completed! 🐙