Computable Univariate Polynomials

This file defines CPolynomial R, the type of canonical univariate polynomials. Canonicality is tracked semantically by requiring the last stored coefficient, when present, to be nonzero.

This provides a unique representation for each polynomial, enabling stronger extensionality properties compared to the raw CPolynomial.Raw type.

@[implicit_reducible]

def CompPoly.CPolynomial (R : Type u_2) [Zero R] : Type u_2

Computable univariate polynomials are represented canonically with no trailing zeros.

A polynomial p : CPolynomial.Raw R is canonical if its last stored coefficient is nonzero whenever the underlying array is nonempty. This gives an instance-stable carrier while keeping the raw normalization algorithms available separately.

Raw.mul defers trimming to the end of its convolution fold (it accumulates with the untrimmed Raw.mulRaw and trims once). Raw.powBySq likewise routes through an untrimmed powBySqUntrimmed and trims once at the top of the repeated-squaring recursion. CPolynomial.divX skips trimming entirely: the input is canonical and extract 1 size only strips from the front, so the leading coefficient (when present) is preserved and the result is already canonical. The division wrappers (divByMonic, modByMonic, modByMonicRemainderOnly, modByMonicByReversal, div, mod) likewise skip the redundant post-trim: each underlying Raw algorithm bottoms out in operations (Raw.add, Raw.sub, subScaledShift) that already trim. CLagrange.basis folds the s.erase i factors with the untrimmed Raw.mulRaw via Quotient.liftOn on the underlying multiset and trims once at the end, and CLagrange.interpolate does the analogous deferred-trim sum via Raw.addRaw/Raw.mulRaw. Remaining opportunities to trim only at the end of an iterative computation: the Array.foldl accumulator in Bivariate/ToPoly.lean (toPoly_foldl_zipIdx_eq_sum), and the two ExtTreeMap.foldl monomial accumulators in Multivariate/Operations.lean. The NTT butterflyStage in Univariate/NTT/Transform.lean is not on this list: it operates on a scalar coefficient Array R and never calls trim.

Equations

• CompPoly.CPolynomial R = { p : CompPoly.CPolynomial.Raw R // p.IsCanonical }

theorem CompPoly.CPolynomial.ext {R : Type u_1} [Zero R] {p q : CPolynomial R} (h : ↑p = ↑q) : p = q

Extensionality for canonical polynomials.

theorem CompPoly.CPolynomial.ext_iff {R : Type u_1} [Zero R] {p q : CPolynomial R} : p = q ↔ ↑p = ↑q

@[instance_reducible]

instance CompPoly.CPolynomial.instCoeRaw {R : Type u_1} [Zero R] : Coe (CPolynomial R) (Raw R)

Canonical polynomials coerce to raw polynomials.

Equations

• CompPoly.CPolynomial.instCoeRaw = { coe := Subtype.val }

@[instance_reducible]

instance CompPoly.CPolynomial.instZero {R : Type u_1} [Zero R] : Zero (CPolynomial R)

The zero polynomial is canonical without any normalization assumptions.

Equations

• CompPoly.CPolynomial.instZero = { zero := ⟨#[], ⋯⟩ }

@[instance_reducible]

instance CompPoly.CPolynomial.instInhabited {R : Type u_1} [Zero R] : Inhabited (CPolynomial R)

The zero polynomial provides the inhabited instance.

Equations

• CompPoly.CPolynomial.instInhabited = { default := 0 }

@[instance_reducible]

instance CompPoly.CPolynomial.instBEq (R : Type u_2) [Zero R] [BEq R] : BEq (CPolynomial R)

CPolynomial R has BEq when R does, comparing the underlying coefficient arrays.

Equations

• CompPoly.CPolynomial.instBEq R = { beq := fun (p q : CompPoly.CPolynomial R) => ↑p == ↑q }

instance CompPoly.CPolynomial.instLawfulBEq (R : Type u_2) [Zero R] [BEq R] [LawfulBEq R] : LawfulBEq (CPolynomial R)

CPolynomial R has LawfulBEq when R does: p == q iff p = q.

@[instance_reducible]

instance CompPoly.CPolynomial.instDecidableEq (R : Type u_2) [Zero R] [DecidableEq R] : DecidableEq (CPolynomial R)

CPolynomial R has DecidableEq when R does, via the underlying Array R representation.

Equations

• CompPoly.CPolynomial.instDecidableEq R = Subtype.instDecidableEq

@[simp]

theorem CompPoly.CPolynomial.trim_eq {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : (↑p).trim = ↑p

Canonical computable polynomials are trim-stable.

@[instance_reducible]

instance CompPoly.CPolynomial.instAddOfLawfulBEq {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : Add (CPolynomial R)

Addition of canonical polynomials (result is canonical).

Equations

• CompPoly.CPolynomial.instAddOfLawfulBEq = { add := fun (p q : CompPoly.CPolynomial R) => ⟨↑p + ↑q, ⋯⟩ }

theorem CompPoly.CPolynomial.add_comm {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p + q = q + p

theorem CompPoly.CPolynomial.add_assoc {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : CPolynomial R) : p + q + r = p + (q + r)

theorem CompPoly.CPolynomial.zero_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : 0 + p = p

theorem CompPoly.CPolynomial.add_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p + 0 = p

def CompPoly.CPolynomial.nsmul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : CPolynomial R) : CPolynomial R

Scalar multiplication by a natural number (result is canonical).

Equations

• CompPoly.CPolynomial.nsmul n p = ⟨CompPoly.CPolynomial.Raw.nsmul n ↑p, ⋯⟩

theorem CompPoly.CPolynomial.nsmul_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : nsmul 0 p = 0

theorem CompPoly.CPolynomial.nsmul_succ {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : CPolynomial R) : nsmul (n + 1) p = nsmul n p + p

@[instance_reducible]

instance CompPoly.CPolynomial.instAddCommSemigroupOfLawfulBEq {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : AddCommSemigroup (CPolynomial R)

Equations

• CompPoly.CPolynomial.instAddCommSemigroupOfLawfulBEq = { toAdd := CompPoly.CPolynomial.instAddOfLawfulBEq, add_assoc := ⋯, add_comm := ⋯ }

@[instance_reducible]

instance CompPoly.CPolynomial.instMulOfLawfulBEq {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : Mul (CPolynomial R)

Multiplication of canonical polynomials.

The product of two canonical polynomials is canonical because multiplication preserves the "no trailing zeros" property.

Equations

• CompPoly.CPolynomial.instMulOfLawfulBEq = { mul := fun (p q : CompPoly.CPolynomial R) => ⟨↑p * ↑q, ⋯⟩ }

theorem CompPoly.CPolynomial.one_is_trimmed {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : Raw.trim 1 = 1

@[instance_reducible]

instance CompPoly.CPolynomial.instOneOfLawfulBEqOfNontrivial {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : One (CPolynomial R)

The constant polynomial 1 is canonical, and is the Unit for multiplication.

This is #[1], which has no trailing zeros.

This proof does not work without the assumption that R is non-trivial.

Equations

• CompPoly.CPolynomial.instOneOfLawfulBEqOfNontrivial = { one := ⟨CompPoly.CPolynomial.Raw.C 1, ⋯⟩ }

instance CompPoly.CPolynomial.instNontrivialOfLawfulBEq {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : Nontrivial (CPolynomial R)

@[reducible]

def CompPoly.CPolynomial.coeff {R : Type u_1} [Zero R] (p : CPolynomial R) (i : ℕ) : R

The coefficient of X^i in the polynomial. Returns 0 if i is out of bounds.

Equations

• p.coeff i = (↑p).coeff i

def CompPoly.CPolynomial.ofArray {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (coeffs : Array R) : CPolynomial R

Build a canonical polynomial from a dense coefficient array.

Equations

• CompPoly.CPolynomial.ofArray coeffs = ⟨CompPoly.CPolynomial.Raw.trim coeffs, ⋯⟩

theorem CompPoly.CPolynomial.coeff_ofArray {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (coeffs : Array R) (i : ℕ) : (ofArray coeffs).coeff i = coeffs.getD i 0

Coefficients of ofArray are exactly the source array entries, with zero default.

def CompPoly.CPolynomial.C {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (r : R) : CPolynomial R

The constant polynomial C r.

Equations

• CompPoly.CPolynomial.C r = ⟨(CompPoly.CPolynomial.Raw.C r).trim, ⋯⟩

def CompPoly.CPolynomial.X {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CPolynomial R

The variable X.

Equations

• CompPoly.CPolynomial.X = ⟨CompPoly.CPolynomial.Raw.X, ⋯⟩

def CompPoly.CPolynomial.linearFactor {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (x : R) : CPolynomial R

The monic linear factor X - C x.

Equations

• CompPoly.CPolynomial.linearFactor x = CompPoly.CPolynomial.C (-x) + CompPoly.CPolynomial.X

def CompPoly.CPolynomial.monomial {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (c : R) : CPolynomial R

Construct a canonical monomial c * X^n as a CPolynomial R.

The result is canonical (no trailing zeros) when c ≠ 0. For example, monomial 2 3 represents 3 * X^2.

Note: If c = 0, this returns 0 (the zero polynomial).

Equations

• CompPoly.CPolynomial.monomial n c = ⟨CompPoly.CPolynomial.Raw.monomial n c, ⋯⟩

def CompPoly.CPolynomial.degree {R : Type u_1} [Zero R] (p : CPolynomial R) : WithBot ℕ

Return the degree of a CPolynomial.

Equations

• p.degree = match Array.size ↑p with | 0 => ⊥ | n.succ => ↑n

def CompPoly.CPolynomial.natDegree {R : Type u_1} [Zero R] (p : CPolynomial R) : ℕ

Natural number degree of a canonical polynomial.

Returns the degree as a natural number. For the zero polynomial, returns 0. This matches Mathlib's Polynomial.natDegree API.

Equations

• p.natDegree = match Array.size ↑p with | 0 => 0 | n.succ => n

def CompPoly.CPolynomial.leadingCoeff {R : Type u_1} [Zero R] (p : CPolynomial R) : R

Return the leading coefficient of a CPolynomial as the last coefficient of the trimmed array, or 0 if the trimmed array is empty.

Equations

• p.leadingCoeff = Array.getLastD (↑p) 0

def CompPoly.CPolynomial.eval {R : Type u_1} [Semiring R] (x : R) (p : CPolynomial R) : R

Evaluate a polynomial at a point.

Equations

• CompPoly.CPolynomial.eval x p = Array.foldl (fun (acc : R) (x_1 : R × ℕ) => match x_1 with | (a, i) => acc + a * x ^ i) 0 (Array.zipIdx ↑p)

def CompPoly.CPolynomial.eval₂ {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial R) : S

Evaluate at x : S via a ring hom f : R →+* S; eval₂ f x p = f(a₀) + f(a₁)*x + f(a₂)*x² + ....

Equations

• CompPoly.CPolynomial.eval₂ f x p = Array.foldl (fun (acc : S) (x_1 : R × ℕ) => match x_1 with | (a, i) => acc + f a * x ^ i) 0 (Array.zipIdx ↑p)

@[inline, specialize #[]]

def CompPoly.CPolynomial.eval₂Horner {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial R) : S

Evaluate at x : S via a ring hom using Horner's method.

Equations

• CompPoly.CPolynomial.eval₂Horner f x p = CompPoly.CPolynomial.Raw.eval₂Horner f x ↑p

@[inline, specialize #[]]

def CompPoly.CPolynomial.evalHorner {R : Type u_1} [Semiring R] (x : R) (p : CPolynomial R) : R

Evaluate a polynomial at a point using Horner's method.

Equations

• CompPoly.CPolynomial.evalHorner x p = CompPoly.CPolynomial.eval₂Horner (RingHom.id R) x p

theorem CompPoly.CPolynomial.eval₂_horner_eq_eval₂ {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (x : S) (p : CPolynomial R) : eval₂Horner f x p = eval₂ f x p

Horner evaluation agrees with the sum-of-powers evaluation.

theorem CompPoly.CPolynomial.eval_horner_eq_eval {R : Type u_1} [Semiring R] (x : R) (p : CPolynomial R) : evalHorner x p = eval x p

Horner evaluation agrees with the sum-of-powers evaluation.

def CompPoly.CPolynomial.support {R : Type u_1} [Zero R] [BEq R] (p : CPolynomial R) : Finset ℕ

The support of a polynomial: indices with nonzero coefficients.

Equations

• p.support = {i ∈ Finset.range (Array.size ↑p) | ((↑p).coeff i != 0) = true}

def CompPoly.CPolynomial.size {R : Type u_1} [Zero R] (p : CPolynomial R) : ℕ

Number of coefficients (length of the underlying array).

Equations

• p.size = Array.size ↑p

def CompPoly.CPolynomial.degreeBound {R : Type u_1} [Zero R] (p : CPolynomial R) : WithBot ℕ

Upper bound on degree: size - 1 if non-empty, ⊥ if empty.

Equations

• p.degreeBound = p.degree

def CompPoly.CPolynomial.natDegreeBound {R : Type u_1} [Zero R] (p : CPolynomial R) : ℕ

Convert degreeBound to a natural number by sending ⊥ to 0.

Equations

• p.natDegreeBound = p.natDegree

def CompPoly.CPolynomial.monic {R : Type u_1} [Zero R] [One R] [BEq R] (p : CPolynomial R) : Bool

Check if a CPolynomial is monic, i.e. its leading coefficient is 1.

Equations

• p.monic = (p.leadingCoeff == 1)

def CompPoly.CPolynomial.divX {R : Type u_1} [Zero R] (p : CPolynomial R) : CPolynomial R

The polynomial with the constant term removed; coeff (divX p) i = coeff p (i + 1).

No post-extract trim is needed: since p is canonical, its last entry is nonzero, and extract 1 p.val.size strips only from the front, so the result is already canonical (vacuously when p.val.size ≤ 1).

Equations

• p.divX = ⟨Array.extract (↑p) 1, ⋯⟩

theorem CompPoly.CPolynomial.coeff_C {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (r : R) (i : ℕ) : (C r).coeff i = if i = 0 then r else 0

Coefficient of the constant polynomial C r.

theorem CompPoly.CPolynomial.coeff_X {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (i : ℕ) : X.coeff i = if i = 1 then 1 else 0

Coefficient of the variable X.

@[simp]

theorem CompPoly.CPolynomial.coeff_zero {R : Type u_1} [Zero R] (i : ℕ) : coeff 0 i = 0

Coefficient of the zero polynomial.

theorem CompPoly.CPolynomial.coeff_one {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (i : ℕ) : coeff 1 i = if i = 0 then 1 else 0

Coefficient of the constant polynomial 1.

theorem CompPoly.CPolynomial.coeff_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (i : ℕ) : (p + q).coeff i = p.coeff i + q.coeff i

Coefficient of a sum.

theorem CompPoly.CPolynomial.coeff_monomial {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n i : ℕ) (c : R) : (monomial n c).coeff i = if i = n then c else 0

Coefficient of a monomial.

theorem CompPoly.CPolynomial.coeff_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (k : ℕ) : (p * q).coeff k = ∑ i ∈ Finset.range (k + 1), p.coeff i * q.coeff (k - i)

Coefficient of a product (convolution sum).

theorem CompPoly.CPolynomial.eq_iff_coeff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial R} : p = q ↔ ∀ (i : ℕ), p.coeff i = q.coeff i

Two polynomials are equal iff they have the same coefficients.

theorem CompPoly.CPolynomial.monomial_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (a b : R) : monomial n (a + b) = monomial n a + monomial n b

Monomials are additive in their coefficient.

theorem CompPoly.CPolynomial.eq_zero_iff_coeff_zero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial R} : p = 0 ↔ ∀ (i : ℕ), p.coeff i = 0

Zero characterization: p = 0 iff all coefficients are zero.

theorem CompPoly.CPolynomial.coeff_eq_zero_of_size_le {R : Type u_1} [Zero R] (p : CPolynomial R) {i : ℕ} (hi : Array.size ↑p ≤ i) : p.coeff i = 0

Coefficients past the stored canonical array are zero.

theorem CompPoly.CPolynomial.coeff_monomial_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (c : R) (p : CPolynomial R) (i : ℕ) : (monomial n c * p).coeff i = if n ≤ i then c * p.coeff (i - n) else 0

Coefficient of a monomial multiple: shift by n and scale by c.

theorem CompPoly.CPolynomial.mem_support_iff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (i : ℕ) : i ∈ p.support ↔ p.coeff i ≠ 0

An index is in the support iff the coefficient there is nonzero.

theorem CompPoly.CPolynomial.support_empty_iff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.support = ∅ ↔ p = 0

The support is empty iff the polynomial is zero.

@[simp]

theorem CompPoly.CPolynomial.C_zero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] : C 0 = 0

The constant polynomial C 0 is zero.

theorem CompPoly.CPolynomial.natDegree_C {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (r : R) : (C r).natDegree = 0

The natDegree of a constant polynomial C r is zero.

theorem CompPoly.CPolynomial.support_C {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {r : R} (hr : r ≠ 0) : (C r).support = {0}

The support of a constant polynomial C r is {0}.

theorem CompPoly.CPolynomial.support_monomial {R : Type u_1} [Semiring R] [DecidableEq R] [BEq R] [LawfulBEq R] {n : ℕ} {c : R} (hc : c ≠ 0) : (monomial n c).support = {n}

The support of a nonzero monomial c * X^n is {n}.

theorem CompPoly.CPolynomial.natDegree_monomial {R : Type u_1} [Semiring R] [DecidableEq R] [BEq R] [LawfulBEq R] {n : ℕ} {c : R} (hc : c ≠ 0) : (monomial n c).natDegree = n

The natDegree of a nonzero monomial c * X^n is n.

theorem CompPoly.CPolynomial.support_add_subset {R : Type u_1} [Semiring R] [DecidableEq R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : (p + q).support ⊆ p.support ∪ q.support

The support of the sum of two polynomials is a subset of the union of their supports.

theorem CompPoly.CPolynomial.eval_eq_sum_support {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (x : R) : eval x p = ∑ i ∈ p.support, p.coeff i * x ^ i

Evaluation equals the sum over support of coefficients times powers.

theorem CompPoly.CPolynomial.eval₂_eq_sum_support {R : Type u_1} {S : Type u_2} [Semiring R] [BEq R] [LawfulBEq R] [Semiring S] (f : R →+* S) (p : CPolynomial R) (x : S) : eval₂ f x p = ∑ i ∈ p.support, f (p.coeff i) * x ^ i

Evaluation via a ring hom equals the sum over support of mapped coefficients times powers.

theorem CompPoly.CPolynomial.coeff_C_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) (c : R) (i : ℕ) : (C c * p).coeff i = c * p.coeff i

theorem CompPoly.CPolynomial.coeff_X_mul_succ {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) (n : ℕ) : (X * p).coeff (n + 1) = p.coeff n

Lemmas on coefficients and multiplication by X.

theorem CompPoly.CPolynomial.coeff_X_mul_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) : (X * p).coeff 0 = 0

theorem CompPoly.CPolynomial.coeff_mul_X_succ {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) (n : ℕ) : (p * X).coeff (n + 1) = p.coeff n

theorem CompPoly.CPolynomial.coeff_mul_X_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) : (p * X).coeff 0 = 0

theorem CompPoly.CPolynomial.coeff_extract_succ {R : Type u_1} [Zero R] (a : Raw R) (i : ℕ) : Raw.coeff (Array.extract a 1) i = a.coeff (i + 1)

theorem CompPoly.CPolynomial.coeff_divX {R : Type u_1} [Zero R] (p : CPolynomial R) (i : ℕ) : p.divX.coeff i = p.coeff (i + 1)

theorem CompPoly.CPolynomial.X_mul_divX_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) : p = X * p.divX + C (p.coeff 0)

theorem CompPoly.CPolynomial.divX_mul_X_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) : p.divX * X + C (p.coeff 0) = p

theorem CompPoly.CPolynomial.divX_size_lt {R : Type u_1} [Zero R] (p : CPolynomial R) (hp : Array.size ↑p > 0) : Array.size ↑p.divX < Array.size ↑p

theorem CompPoly.CPolynomial.induction_on {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {P : CPolynomial R → Prop} (p : CPolynomial R) (h0 : P 0) (hC : ∀ (a : R), P (C a)) (hadd : ∀ (p q : CPolynomial R), P p → P q → P (p + q)) (hX : ∀ (p : CPolynomial R), P p → P (X * p)) : P p

Induction principle for polynomials (mirrors mathlib's Polynomial.induction_on).

theorem CompPoly.CPolynomial.degree_eq_support_max_aux_degree {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) {k : Fin (Array.size ↑p)} (hk : (↑p).lastNonzero = some k) : p.degree = ↑↑k

Lemma for degree_eq_support_max: degree in terms of lastNonzero.

theorem CompPoly.CPolynomial.degree_eq_support_max_aux_lastNonzero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (hp : p ≠ 0) : ∃ (k : Fin (Array.size ↑p)), (↑p).lastNonzero = some k

theorem CompPoly.CPolynomial.degree_eq_support_max_aux_mem_support {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) {k : Fin (Array.size ↑p)} (hk : (↑p).lastNonzero = some k) : ↑k ∈ p.support

theorem CompPoly.CPolynomial.degree_eq_support_max {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (hp : p ≠ 0) : ∃ n ∈ p.support, p.degree = ↑n

Degree equals the maximum of the support when the polynomial is non-zero. Here p.degree = some n where n is the maximum index in p.support.

theorem CompPoly.CPolynomial.degree_eq_natDegree {R : Type u_1} [Zero R] (p : CPolynomial R) (hp : p ≠ 0) : p.degree = ↑p.natDegree

When p ≠ 0, degree p equals natDegree p (as WithBot ℕ).

theorem CompPoly.CPolynomial.degree_zero {R : Type u_1} [Zero R] : degree 0 = ⊥

Lemma for computing the degree of 0 in proofs.

theorem CompPoly.CPolynomial.natDegree_eq_support_sup {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.natDegree = p.support.sup fun (n : ℕ) => n

The natural degree is the maximum element of the support.

theorem CompPoly.CPolynomial.le_natDegree_of_ne_zero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial R} {i : ℕ} (h : p.coeff i ≠ 0) : i ≤ p.natDegree

If coeff p i ≠ 0 then i ≤ p.natDegree.

theorem CompPoly.CPolynomial.natDegree_add_le {R : Type u_1} [Semiring R] [DecidableEq R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : (p + q).natDegree ≤ max p.natDegree q.natDegree

The natDegree of a sum is at most the max of the natDegrees.

theorem CompPoly.CPolynomial.leadingCoeff_ne_zero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial R} (h : p ≠ 0) : p.leadingCoeff ≠ 0

The leading coefficient of a nonzero polynomial is nonzero.

def CompPoly.CPolynomial.divByMonic {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (p q : CPolynomial R) : CPolynomial R

Quotient of p by a monic polynomial q. Matches Mathlib's Polynomial.divByMonic.

Equations

• p.divByMonic q = ⟨(↑p).divByMonic ↑q, ⋯⟩

def CompPoly.CPolynomial.modByMonic {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (p q : CPolynomial R) : CPolynomial R

Remainder of p modulo a monic polynomial q. Matches Mathlib's Polynomial.modByMonic.

Equations

• p.modByMonic q = ⟨(↑p).modByMonic ↑q, ⋯⟩

def CompPoly.CPolynomial.modByMonicRemainderOnly {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R

Remainder of p modulo a monic polynomial q, using a remainder-only implementation.

Equations

• p.modByMonicRemainderOnly q = ⟨(↑p).modByMonicRemainderOnly ↑q, ⋯⟩

def CompPoly.CPolynomial.modByMonicByReversal {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (M : Raw.MulLowContext R) (p q : CPolynomial R) : CPolynomial R

Remainder of p modulo a monic polynomial q, using reversal and low products.

Equations

• CompPoly.CPolynomial.modByMonicByReversal M p q = ⟨CompPoly.CPolynomial.Raw.modByMonicByReversal M ↑p ↑q, ⋯⟩

theorem CompPoly.CPolynomial.modByMonicRemainderOnly_eq_modByMonic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p.modByMonicRemainderOnly q = p.modByMonic q

The remainder-only monic remainder agrees with the canonical monic remainder.

def CompPoly.CPolynomial.div {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R

Quotient of p by q (when R is a field).

Equations

• p.div q = ⟨(↑p).div ↑q, ⋯⟩

@[simp]

theorem CompPoly.CPolynomial.div_zero {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.div 0 = 0

Any CPolynomial divided by the zero polynomial gives the zero polynomial.

def CompPoly.CPolynomial.mod {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R

Remainder of p modulo q (when R is a field).

Equations

• p.mod q = ⟨(↑p).mod ↑q, ⋯⟩

@[simp]

theorem CompPoly.CPolynomial.mod_zero {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.mod 0 = 0

Any CPolynomial modulo the zero polynomial gives the zero polynomial.

@[instance_reducible]

instance CompPoly.CPolynomial.instDivOfLawfulBEq {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] : Div (CPolynomial R)

Equations

• CompPoly.CPolynomial.instDivOfLawfulBEq = { div := CompPoly.CPolynomial.div }

@[instance_reducible]

instance CompPoly.CPolynomial.instModOfLawfulBEq {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] : Mod (CPolynomial R)

Equations

• CompPoly.CPolynomial.instModOfLawfulBEq = { mod := CompPoly.CPolynomial.mod }

def CompPoly.CPolynomial.monicNormalize {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : CPolynomial R

Normalize a nonzero polynomial to monic form. The zero polynomial stays zero.

Equations

• p.monicNormalize = CompPoly.CPolynomial.ofArray (↑p).monicNormalize

def CompPoly.CPolynomial.gcdMonicWithFuel {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] : ℕ → CPolynomial R → CPolynomial R → CPolynomial R

Euclidean gcd with explicit fuel, normalized to a monic result.

Equations

• CompPoly.CPolynomial.gcdMonicWithFuel x✝² x✝¹ x✝ = CompPoly.CPolynomial.ofArray (CompPoly.CPolynomial.Raw.gcdMonicWithFuel x✝² ↑x✝¹ ↑x✝)

def CompPoly.CPolynomial.gcdMonic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : CPolynomial R

Monic Euclidean gcd for canonical univariate polynomials.

Equations

• p.gcdMonic q = CompPoly.CPolynomial.ofArray ((↑p).gcdMonic ↑q)

theorem CompPoly.CPolynomial.one_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) : 1 * p = p

theorem CompPoly.CPolynomial.mul_one {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) : p * 1 = p

theorem CompPoly.CPolynomial.mul_assoc {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : CPolynomial R) : p * q * r = p * (q * r)

theorem CompPoly.CPolynomial.zero_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : 0 * p = 0

theorem CompPoly.CPolynomial.mul_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p * 0 = 0

theorem CompPoly.CPolynomial.mul_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : CPolynomial R) : p * (q + r) = p * q + p * r

theorem CompPoly.CPolynomial.add_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : CPolynomial R) : (p + q) * r = p * r + q * r

theorem CompPoly.CPolynomial.pow_is_trimmed {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Raw R) (n : ℕ) : (p ^ n).trim = p ^ n

theorem CompPoly.CPolynomial.pow_succ_right {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : Raw R) (n : ℕ) : p ^ (n + 1) = p ^ n * p

@[instance_reducible]

instance CompPoly.CPolynomial.instAddCommMonoidOfLawfulBEq {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : AddCommMonoid (CPolynomial R)

CPolynomial R forms a commutative monoid when R is a semiring.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance CompPoly.CPolynomial.instSemiringOfLawfulBEqOfNontrivial {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : Semiring (CPolynomial R)

CPolynomial R forms a semiring when R is a semiring.

The semiring structure extends the AddCommGroup structure with multiplication. All operations preserve the canonical property (no trailing zeros).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompPoly.CPolynomial.natCast_eq_C {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (n : ℕ) : ↑n = C ↑n

theorem CompPoly.CPolynomial.val_pow {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) (n : ℕ) : ↑(p ^ n) = ↑p ^ n

The underlying Raw value of p ^ n equals p.val ^ n (using the Raw Pow instance). This bridges the optimized powBySq used in the Semiring instance with the spec pow.

theorem CompPoly.CPolynomial.C_mul_X_pow_eq_monomial {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] [Nontrivial R] (r : R) (n : ℕ) : C r * X ^ n = monomial n r

C r * X^n = monomial n r as canonical polynomials.

theorem CompPoly.CPolynomial.coeff_finset_sum {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (f : ι → CPolynomial R) (n : ℕ) : (s.sum f).coeff n = ∑ i ∈ s, (f i).coeff n

Distribute CPolynomial.coeff over a Finset.sum.

theorem CompPoly.CPolynomial.mul_comm {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p * q = q * p

@[instance_reducible]

instance CompPoly.CPolynomial.instCommSemiringOfLawfulBEqOfNontrivial {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CommSemiring (CPolynomial R)

CPolynomial R forms a commutative semiring when R is a commutative semiring.

Commutativity follows from the commutativity of multiplication in the base ring.

Equations

• CompPoly.CPolynomial.instCommSemiringOfLawfulBEqOfNontrivial = { toSemiring := inferInstance, mul_comm := ⋯ }

@[instance_reducible]

instance CompPoly.CPolynomial.instNegOfLawfulBEq {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] : Neg (CPolynomial R)

Equations

• CompPoly.CPolynomial.instNegOfLawfulBEq = { neg := fun (p : CompPoly.CPolynomial R) => ⟨-↑p, ⋯⟩ }

@[instance_reducible]

instance CompPoly.CPolynomial.instSubOfLawfulBEq {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] : Sub (CPolynomial R)

Equations

• CompPoly.CPolynomial.instSubOfLawfulBEq = { sub := fun (p q : CompPoly.CPolynomial R) => p + -q }

def CompPoly.CPolynomial.erase {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (n : ℕ) (p : CPolynomial R) : CPolynomial R

Erase the coefficient at index n (same as p except coeff n = 0, then trimmed).

Uses an in-place Array.setIfInBounds and avoids allocating a length-n monomial array plus the padding/zip passes of sub.

Equations

• CompPoly.CPolynomial.erase n p = ⟨CompPoly.CPolynomial.Raw.trim (Array.setIfInBounds (↑p) n 0), ⋯⟩

theorem CompPoly.CPolynomial.coeff_erase {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (n i : ℕ) (p : CPolynomial R) : (erase n p).coeff i = if i = n then 0 else p.coeff i

Coefficient of erase n p: zero at n, otherwise coeff p i.

theorem CompPoly.CPolynomial.leadingCoeff_eq_coeff_natDegree {R : Type u_1} [Zero R] (p : CPolynomial R) : p.leadingCoeff = p.coeff p.natDegree

Leading coefficient equals the coefficient at natDegree.

theorem CompPoly.CPolynomial.monomial_add_erase {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] (p : CPolynomial R) : p = monomial p.natDegree p.leadingCoeff + erase p.natDegree p

A polynomial equals its leading monomial plus the rest (erase at natDegree).

theorem CompPoly.CPolynomial.coeff_neg {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (i : ℕ) : (-p).coeff i = -p.coeff i

theorem CompPoly.CPolynomial.coeff_sub {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (i : ℕ) : (p - q).coeff i = p.coeff i - q.coeff i

def CompPoly.CPolynomial.subMulMonomial {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (a : CPolynomial R) (c : R) (d : ℕ) (b : CPolynomial R) : CPolynomial R

Fused a - c * X^d * b on canonical coefficient arrays.

Each output coefficient is computed directly, so one call costs O(max (deg a) (d + deg b)) field operations instead of the O(d * deg b) convolution behind monomial d c * b followed by a subtraction pass. The guards skip the array construction entirely when either factor is zero.

Equations

• One or more equations did not get rendered due to their size.

theorem CompPoly.CPolynomial.subMulMonomial_eq {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] (a : CPolynomial R) (c : R) (d : ℕ) (b : CPolynomial R) : a.subMulMonomial c d b = a - monomial d c * b

subMulMonomial agrees with the generic a - monomial d c * b.

theorem CompPoly.CPolynomial.erase_correct {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (p : CPolynomial R) : erase n p = p - monomial n (p.coeff n)

The in-place erase agrees with the subtraction-based characterization: erase n p equals p - monomial n (p.coeff n).

theorem CompPoly.CPolynomial.neg_add_cancel {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : -p + p = 0

@[instance_reducible]

instance CompPoly.CPolynomial.instAddCommGroupOfLawfulBEq {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] : AddCommGroup (CPolynomial R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance CompPoly.CPolynomial.instRingOfLawfulBEqOfNontrivial {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [Nontrivial R] : Ring (CPolynomial R)

CPolynomial R forms a ring when R is a ring.

The ring structure extends the semiring structure with negation and subtraction. Most of the structure is already provided by the Semiring instance.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance CompPoly.CPolynomial.instCommRingOfLawfulBEqOfNontrivial {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] : CommRing (CPolynomial R)

CPolynomial R forms a commutative ring when R is a commutative ring.

This combines the CommSemiring and Ring structures.

Equations

• CompPoly.CPolynomial.instCommRingOfLawfulBEqOfNontrivial = { toRing := inferInstance, mul_comm := ⋯ }

@[instance_reducible]

instance CompPoly.CPolynomial.smul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : SMul R (CPolynomial R)

Scalar multiplication for canonical polynomials: multiply each coefficient by r, then trim to restore canonicity.

Equations

• CompPoly.CPolynomial.smul = { smul := fun (r : R) (p : CompPoly.CPolynomial R) => ⟨(CompPoly.CPolynomial.Raw.smul r ↑p).trim, ⋯⟩ }

theorem CompPoly.CPolynomial.coeff_smul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r : R) (p : CPolynomial R) (i : ℕ) : (r • p).coeff i = r * p.coeff i

Coefficient of a scalar multiple.

theorem CompPoly.CPolynomial.smul_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r : R) : r • 0 = 0

Scalar multiplication on 0 gives 0.

theorem CompPoly.CPolynomial.smul_eq_of_coeff_eq {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p q : CPolynomial R} (h : Raw.Trim.equiv ↑p ↑q) : p = q

Helper lemma: Two CPolynomials are equal if the underlying Raw CPolynomials are trim equivalent.

theorem CompPoly.CPolynomial.smul_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r : R) (p q : CPolynomial R) : r • (p + q) = r • p + r • q

Scalar multiplication distributes.

theorem CompPoly.CPolynomial.add_smul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r s : R) (p : CPolynomial R) : (r + s) • p = r • p + s • p

Scalar multiplication distributes across scalar addition.

theorem CompPoly.CPolynomial.zero_smul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : 0 • p = 0

Scalar multiplication by 0 gives 0.

theorem CompPoly.CPolynomial.one_smul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : 1 • p = p

Scalar multiplication on p by 1 gives p.

theorem CompPoly.CPolynomial.mul_smul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r s : R) (p : CPolynomial R) : (r * s) • p = r • s • p

Scalar multiplication is associative.

@[instance_reducible]

instance CompPoly.CPolynomial.instModule {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : Module R (CPolynomial R)

CPolynomial forms a module when R is a semiring.

Equations

• CompPoly.CPolynomial.instModule = { toSMul := CompPoly.CPolynomial.smul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

theorem CompPoly.CPolynomial.div_eq_divByMonic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p.div q = (q.leadingCoeff⁻¹ • p).divByMonic (q.leadingCoeff⁻¹ • q)

Equality between div and divByMonic for CPolynomial R

theorem CompPoly.CPolynomial.mod_eq_modByMonic {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p.mod q = (q.leadingCoeff⁻¹ • p).modByMonic (q.leadingCoeff⁻¹ • q)

Equality between mod and modByMonic for CPolynomial R