Univariate polynomials over the rationals

Mathematical statement

A univariate polynomial in Q[x] is represented by finitely many rational coefficients a_k as p(x)=a_0+a_1x+⋯+a_nx^n, with nonnegative integer exponents. The degree of a nonzero polynomial is the largest index with a nonzero coefficient; this entry calls the degree of the zero polynomial undefined.

Representative formula (exact TeX)

x^{n}

Assumptions

• Fix a formal indeterminate x, rational coefficients, and finite support.
• Coefficient vectors [a_0,a_1,…] are ordered from lowest to highest power. Trailing zeros do not change the polynomial.

Symbol scope

• x — formal indeterminate
• n — nonnegative integer exponent of the representative monomial

Intuition, definition, and misconceptions

A polynomial is not determined by the number of written terms. First add coefficients of equal powers: for example, x²−x²+3 becomes the nonzero constant 3 of degree zero. The zero polynomial is distinct from a nonzero constant polynomial.

Addition adds coefficients of each power. Multiplication combines terms with equal sums of exponents, giving finite convolution. Evaluation uses the same coefficient data at a particular input; equality at one input does not establish a polynomial identity.

The exercises use exact integer coefficients and integer inputs. A coefficient beyond the finite support is zero. Calling the zero polynomial degree undefined is a teaching convention; a future bridge must distinguish Mathlib degree, whose value is ⊥, from natDegree, whose value is zero in that case.

Common errors include taking the highest written exponent before combining like terms, or using vector length and trailing zeros to determine degree.

Adopted derivation guide

The original MKO is retained. The guide has its own append-only revision and verification boundaries, not a new Lean proof.

Prerequisites

• Variables and algebraic expressions — Distinguish a formal expression from evaluation at a specified input.
• Natural-number powers and principal square roots — Polynomial terms use nonnegative integer powers.
• Rational number — The coefficient field is explicitly the rationals.

Verification boundary

Finite coefficients can be verified individually; the semantic bridge for polynomial data, evaluation, and degree is not yet formalized.

not_formalized

This does not mean the content is false; it means no replayable computational or formal evidence is registered yet.

Next obligation

Bind Polynomial Q, coeff, eval, degree, and the zero-polynomial distinction from natDegree.

Same-source structured data

This page and the interactive view use the same object and existing language edition; this adds no proof or human review.