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.

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.

TODO optimizations may be had by trimming only at the end of iterative operations

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

@[implicit_reducible]

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

Canonical polynomials coerce to raw polynomials.

@[implicit_reducible]

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

The zero polynomial is canonical without any normalization assumptions.

@[implicit_reducible]

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

The zero polynomial provides the inhabited instance.

@[implicit_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.

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.

@[implicit_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.

@[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.

@[implicit_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).

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).

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

@[implicit_reducible]

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

@[implicit_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.

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

@[implicit_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.

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.

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

The constant polynomial C r.

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

The variable 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).

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

Return the degree of a CPolynomial.

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.

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.

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

Evaluate a polynomial at a point.

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² + ....

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.

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

Number of coefficients (length of the underlying array).

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.

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

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

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.

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

The polynomial with the constant term removed; coeff (divX p) i = coeff p (i + 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.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.

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] [BEq R] [LawfulBEq 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] [BEq R] [LawfulBEq 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.

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

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

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

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

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).

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).

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_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.

@[implicit_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).

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.mul_comm {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : p * q = q * p

@[implicit_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.

@[implicit_reducible]

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

@[implicit_reducible]

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

theorem CompPoly.CPolynomial.erase_canonical {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (p : CPolynomial R) : have e := ↑p - Raw.monomial n ((↑p).coeff n); e.trim = e

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

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

theorem CompPoly.CPolynomial.coeff_erase {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [DecidableEq 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

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

@[implicit_reducible]

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

@[implicit_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.

@[implicit_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.

@[implicit_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.

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.

@[implicit_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.