Raw Univariate Polynomial Proofs

Proofs about operations on raw computable univariate polynomials.

theorem CompPoly.CPolynomial.Raw.pow_zero {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) : p ^ 0 = C 1

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

theorem CompPoly.CPolynomial.Raw.matchSize_size_eq {Q : Type u_2} [Semiring Q] {p q : Raw Q} : match Array.matchSize p q 0 with | (p', q') => p'.size = q'.size

theorem CompPoly.CPolynomial.Raw.matchSize_size {Q : Type u_2} [Semiring Q] {p q : Raw Q} : match Array.matchSize p q 0 with | (p', snd) => p'.size = max (Array.size p) (Array.size q)

theorem CompPoly.CPolynomial.Raw.zipWith_size {R : Type u_4} {f : R → R → R} {a b : Array R} (h : a.size = b.size) : (Array.zipWith f a b).size = a.size

theorem CompPoly.CPolynomial.Raw.concat_coeff₁ {R : Type u_1} [Semiring R] (p q : Raw R) (i : ℕ) : i < Array.size p → (p ++ q).coeff i = p.coeff i

theorem CompPoly.CPolynomial.Raw.concat_coeff₂ {R : Type u_1} [Semiring R] (p q : Raw R) (i : ℕ) : i ≥ Array.size p → (p ++ q).coeff i = q.coeff (i - Array.size p)

theorem CompPoly.CPolynomial.Raw.add_size {Q : Type u_2} [Semiring Q] {p q : Raw Q} : Array.size (p.addRaw q) = max (Array.size p) (Array.size q)

theorem CompPoly.CPolynomial.Raw.add_coeff {Q : Type u_2} [Semiring Q] {p q : Raw Q} {i : ℕ} (hi : i < Array.size (p.addRaw q)) : (p.addRaw q)[i] = p.coeff i + q.coeff i

theorem CompPoly.CPolynomial.Raw.add_coeff? {Q : Type u_2} [Semiring Q] (p q : Raw Q) (i : ℕ) : (p.addRaw q).coeff i = p.coeff i + q.coeff i

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

theorem CompPoly.CPolynomial.Raw.add_equiv_raw {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : Trim.equiv (p.add q) (p.addRaw q)

theorem CompPoly.CPolynomial.Raw.smul_equiv {R : Type u_1} [Semiring R] (p : Raw R) (i : ℕ) (r : R) : (smul r p).coeff i = r * p.coeff i

theorem CompPoly.CPolynomial.Raw.nsmulRaw_equiv {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) [LawfulBEq R] (n i : ℕ) : (nsmulRaw n p).trim.coeff i = ↑n * p.trim.coeff i

theorem CompPoly.CPolynomial.Raw.mul_pow_assoc {R : Type u_1} [Semiring R] [BEq R] (p : Raw R) (n : ℕ) (q : Raw R) (m l : ℕ) : l + m = n → p.mul^[n] q = p.mul^[m] (p.mul^[l] q)

theorem CompPoly.CPolynomial.Raw.mul_pow_succ {R : Type u_1} [Semiring R] [BEq R] (p q : Raw R) (n : ℕ) : p.mul^[n + 1] q = p.mul (p.mul^[n] q)

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

@[simp]

theorem CompPoly.CPolynomial.Raw.zero_def {Q : Type u_2} : 0 = #[]

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

theorem CompPoly.CPolynomial.Raw.zero_canonical {R : Type u_1} [Semiring R] [BEq R] : trim 0 = 0

@[simp]

theorem CompPoly.CPolynomial.Raw.leadingCoeff_zero {R : Type u_1} [Semiring R] [BEq R] : leadingCoeff 0 = 0

theorem CompPoly.CPolynomial.Raw.monomial_canonical {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (c : R) : (monomial n c).trim = monomial n c

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

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

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

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

@[simp]

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

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

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

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

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

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

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

theorem CompPoly.CPolynomial.Raw.foldl_preserves_canonical {R : Type u_1} [Semiring R] [BEq R] {α : Type u_4} (f : Raw R → α → Raw R) (z : Raw R) (as : Array α) (hz : z.trim = z) (hf : ∀ (acc : Raw R) (x : α), (f acc x).trim = f acc x) : (Array.foldl f z as).trim = Array.foldl f z as

theorem CompPoly.CPolynomial.Raw.coeff_foldl_add {R : Type u_1} [Semiring R] [BEq R] {α : Type u_4} [LawfulBEq R] (l : List α) (f : α → Raw R) (z : Raw R) (k : ℕ) : (List.foldl (fun (acc : Raw R) (x : α) => acc + f x) z l).coeff k = z.coeff k + (List.map (fun (x : α) => (f x).coeff k) l).sum

theorem CompPoly.CPolynomial.Raw.coeff_foldl_addRaw {R : Type u_1} [Semiring R] [BEq R] {α : Type u_4} [LawfulBEq R] (l : List α) (f : α → Raw R) (z : Raw R) (k : ℕ) : (List.foldl (fun (acc : Raw R) (x : α) => acc.addRaw (f x)) z l).coeff k = z.coeff k + (List.map (fun (x : α) => (f x).coeff k) l).sum

Coefficient of an untrimmed addRaw accumulator fold: the same statement as coeff_foldl_add, but the partial sums are combined with addRaw (no per-step trim). This is what mulRaw folds with.

theorem CompPoly.CPolynomial.Raw.mul_eq_foldl {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : p * q = Array.foldl (fun (acc : Raw R) (x : R × ℕ) => match x with | (a, i) => acc + mulPowX i (smul a q)) (mk #[]) (Array.zipIdx p)

mul agrees with the trimmed-add convolution fold (the previous definition of mul). mul now folds with the untrimmed addRaw and trims once at the end; this lemma is the bridge that lets the existing coefficient and equivalence proofs go through unchanged.

theorem CompPoly.CPolynomial.Raw.sum_zipIdx_eq_sum_range {R : Type u_1} [Semiring R] {α : Type u_4} [AddCommMonoid α] (p : Raw R) (f : R → ℕ → α) : (List.map (fun (x : R × ℕ) => match x with | (a, i) => f a i) (Array.zipIdx p).toList).sum = ∑ i ∈ Finset.range (Array.size p), f (p.coeff i) i

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

theorem CompPoly.CPolynomial.Raw.sum_range_extend {R : Type u_1} [Semiring R] (p q : Raw R) (k : ℕ) : (∑ i ∈ Finset.range (Array.size p), if k < i then 0 else p.coeff i * q.coeff (k - i)) = ∑ i ∈ Finset.range (k + 1), p.coeff i * q.coeff (k - i)

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

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

theorem CompPoly.CPolynomial.Raw.nsmulRawSucc {Q : Type u_2} [Semiring Q] (n : ℕ) (p : Raw Q) : nsmulRaw (n + 1) p = (nsmulRaw n p).addRaw p

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

theorem CompPoly.CPolynomial.Raw.smul_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a : R) (p : Raw R) (k : ℕ) : (smul a p).coeff k = a * p.coeff k

theorem CompPoly.CPolynomial.Raw.smul_addRaw_distrib {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a' : R) (q r : Raw R) : smul a' (q.addRaw r) = (smul a' q).addRaw (smul a' r)

theorem CompPoly.CPolynomial.Raw.smul_distrib_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a' : R) (q r : Raw R) : (smul a' (q + r)).trim = smul a' q + smul a' r

theorem CompPoly.CPolynomial.Raw.coeff_smul_add_distrib {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a : R) (q r : Raw R) (i : ℕ) : (smul a (q + r)).coeff i = (smul a q).coeff i + (smul a r).coeff i

theorem CompPoly.CPolynomial.Raw.coeff_add_smul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a b : R) (q : Raw R) (k : ℕ) : (smul (a + b) q).coeff k = (smul a q).coeff k + (smul b q).coeff k

theorem CompPoly.CPolynomial.Raw.coeff_sum {R : Type u_1} [Semiring R] (p : Raw R) (k : ℕ) : (Array.map (fun (x : R × ℕ) => match x with | (a, i) => (mulPowX i (smul a 1)).coeff k) (Array.zipIdx p)).sum = p.coeff k

theorem CompPoly.CPolynomial.Raw.coeff_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : (p * q).coeff k = (List.map (fun (x : R × ℕ) => match x with | (a, i) => (mulPowX i (smul a q)).coeff k) (Array.zipIdx p).toList).sum

theorem CompPoly.CPolynomial.Raw.coeff_mulPowX {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (i : ℕ) (p : Raw R) (k : ℕ) : (mulPowX i p).coeff k = if k < i then 0 else p.coeff (k - i)

theorem CompPoly.CPolynomial.Raw.coeff_mulPowX' {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) (n i : ℕ) : (mulPowX n p).coeff i = if i < n then 0 else p.coeff (i - n)

theorem CompPoly.CPolynomial.Raw.mulPowX_coeff' {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) (n k : ℕ) : (mulPowX n p).coeff k = if k < n then 0 else p.coeff (k - n)

theorem CompPoly.CPolynomial.Raw.coeff_mulPowX_smul_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (i : ℕ) (a b : R) (q : Raw R) (k : ℕ) : (mulPowX i (smul (a + b) q)).coeff k = (mulPowX i (smul a q)).coeff k + (mulPowX i (smul b q)).coeff k

theorem CompPoly.CPolynomial.Raw.mulPowX_zero {R : Type u_1} [Semiring R] (p : Raw R) : mulPowX 0 p = p

theorem CompPoly.CPolynomial.Raw.equiv_mul_one {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : Trim.equiv (p * 1) p

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

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

Raw.add trims at the end of its accumulation, so its output is canonical.

theorem CompPoly.CPolynomial.Raw.coeff_mul_eq_sum_range {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k n : ℕ) (h : Array.size p ≤ n) : (p * q).coeff k = (List.map (fun (i : ℕ) => (mulPowX i (smul (p.coeff i) q)).coeff k) (List.range n)).sum

theorem CompPoly.CPolynomial.Raw.C_mul_eq_smul_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r : R) (q : Raw R) : C r * q = (smul r q).trim

theorem CompPoly.CPolynomial.Raw.smul_one_eq_self {R : Type u_1} [Semiring R] (p : Raw R) : smul 1 p = p

theorem CompPoly.CPolynomial.Raw.smul_zero_eq_replicate_zero {R : Type u_1} [Semiring R] (p : Raw R) : smul 0 p = mk (Array.replicate (Array.size p) 0)

theorem CompPoly.CPolynomial.Raw.trim_replicate_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) : (mk (Array.replicate n 0)).trim = 0

theorem CompPoly.CPolynomial.Raw.smul_zero_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : (smul 0 p).trim = 0

theorem CompPoly.CPolynomial.Raw.X_mul_eq_mulX_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) : X * p = p.mulX.trim

theorem CompPoly.CPolynomial.Raw.mulX_monomial_one {R : Type u_1} [Semiring R] [BEq R] [DecidableEq R] [LawfulBEq R] [Nontrivial R] (n : ℕ) : (monomial n 1).mulX = monomial (n + 1) 1

theorem CompPoly.CPolynomial.Raw.X_pow_eq_monomial_one {R : Type u_1} [Semiring R] [BEq R] [DecidableEq R] [LawfulBEq R] [Nontrivial R] (n : ℕ) : X ^ n = monomial n 1

theorem CompPoly.CPolynomial.Raw.smul_monomial_one_trim {R : Type u_1} [Semiring R] [BEq R] [DecidableEq R] [LawfulBEq R] [Nontrivial R] (n : ℕ) (r : R) : (smul r (monomial n 1)).trim = monomial n r

theorem CompPoly.CPolynomial.Raw.smul_mulPowX_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a : R) (q : Raw R) (i k : ℕ) : (mulPowX i (smul a q)).coeff k = if k < i then 0 else a * q.coeff (k - i)

theorem CompPoly.CPolynomial.Raw.mul_coeff_list {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : (p * q).coeff k = (List.map (fun (x : R × ℕ) => match x with | (a, i) => if k < i then 0 else a * q.coeff (k - i)) (Array.zipIdx p).toList).sum

theorem CompPoly.CPolynomial.Raw.mul_coeff_range_size {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : (p * q).coeff k = ∑ i ∈ Finset.range (Array.size p), if k < i then 0 else p.coeff i * q.coeff (k - i)

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

def CompPoly.CPolynomial.Raw.MulLowContext.convolution {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : MulLowContext R

Low-product backend using the coefficient convolution formula.

theorem CompPoly.CPolynomial.Raw.truncate_coeff {R : Type u_1} [Semiring R] (k : ℕ) (p : Raw R) (i : ℕ) : (truncate k p).coeff i = if i < k then p.coeff i else 0

def CompPoly.CPolynomial.Raw.MulLowContext.naive {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] : MulLowContext R

Low-product backend using ordinary multiplication followed by truncation.

theorem CompPoly.CPolynomial.Raw.reverse_coeff {R : Type u_1} [Semiring R] (n : ℕ) (p : Raw R) (i : ℕ) : (reverse n p).coeff i = if i < n then p.coeff (n - 1 - i) else 0

theorem CompPoly.CPolynomial.Raw.mulLow_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (M : MulLowContext R) (k : ℕ) (p q : Raw R) (i : ℕ) : (M.mulLow k p q).coeff i = if i < k then (p * q).coeff i else 0

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

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

theorem CompPoly.CPolynomial.Raw.mul_assoc_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) (n : ℕ) : (p * q * r).coeff n = (p * (q * r)).coeff n

theorem CompPoly.CPolynomial.Raw.mul_assoc_equiv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q r : Raw R) : Trim.equiv (p * q * r) (p * (q * r))

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

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

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

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

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

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

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

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

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

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

theorem CompPoly.CPolynomial.Raw.mul_comm_coeff {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (k : ℕ) : (p * q).coeff k = (q * p).coeff k

theorem CompPoly.CPolynomial.Raw.mul_comm_equiv {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : Trim.equiv (p * q) (q * p)

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

theorem CompPoly.CPolynomial.Raw.neg_coeff {R : Type u_3} [NegZeroClass R] (p : Raw R) (i : ℕ) : p.neg.coeff i = -p.coeff i

theorem CompPoly.CPolynomial.Raw.neg_trim {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (p : Raw R) : p.trim = p → (-p).trim = -p

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

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

theorem CompPoly.CPolynomial.Raw.sub_is_trimmed {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (p q : Raw R) : (p - q).trim = p - q

Raw.sub reduces to p + -q, whose final add step trims, so the result is canonical.

theorem CompPoly.CPolynomial.Raw.coeff_mul_X_pow {R : Type u_1} [BEq R] [CommRing R] [Nontrivial R] [LawfulBEq R] (p : Raw R) (n i : ℕ) : (p * X ^ n).coeff i = if n ≤ i ∧ i - n < Array.size p then p.coeff (i - n) else 0

theorem CompPoly.CPolynomial.Raw.coeff_C_mul_X_pow {R : Type u_1} [BEq R] [CommRing R] [Nontrivial R] [LawfulBEq R] (scale : R) (p : Raw R) (n i : ℕ) : (C scale * (p * X ^ n)).coeff i = if n ≤ i ∧ i - n < Array.size p then scale * p.coeff (i - n) else 0

theorem CompPoly.CPolynomial.Raw.subScaledShift_eq_sub_C_mul_X_pow {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (p q : Raw R) (scale : R) (shift : ℕ) (hsize : shift + Array.size q ≤ Array.size p) : p.subScaledShift q scale shift = (p - C scale * (q * X ^ shift)).trim

theorem CompPoly.CPolynomial.Raw.modByMonicRemainderOnly_go_eq_divModByMonicAux_go_snd {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (n : ℕ) (p q : Raw R) : modByMonicRemainderOnly.go n p q = (divModByMonicAux.go n p q).2

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

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

theorem CompPoly.CPolynomial.Raw.divModByMonicAux_go_fst_canonical {R : Type u_1} [BEq R] [CommRing R] [LawfulBEq R] (n : ℕ) (p q : Raw R) : (divModByMonicAux.go n p q).1.trim = (divModByMonicAux.go n p q).1

The quotient produced by the monic long-division recursion is canonical regardless of input: each non-base step accumulates via Raw.add (which trims), and the base case returns 0.

theorem CompPoly.CPolynomial.Raw.divModByMonicAux_go_snd_canonical {R : Type u_1} [BEq R] [CommRing R] [LawfulBEq R] (n : ℕ) (p q : Raw R) : p.trim = p → (divModByMonicAux.go n p q).2.trim = (divModByMonicAux.go n p q).2

The remainder produced by the monic long-division recursion is canonical when the input is. Each recursive step feeds the next call a trimmed (p - q').trim, and the base case returns the input unchanged.

theorem CompPoly.CPolynomial.Raw.divByMonic_canonical {R : Type u_1} [BEq R] [CommRing R] [LawfulBEq R] (p q : Raw R) : (p.divByMonic q).trim = p.divByMonic q

Raw.divByMonic returns a canonical polynomial regardless of whether p is canonical.

theorem CompPoly.CPolynomial.Raw.modByMonic_canonical {R : Type u_1} [BEq R] [CommRing R] [LawfulBEq R] {p : Raw R} (hp : p.trim = p) (q : Raw R) : (p.modByMonic q).trim = p.modByMonic q

Raw.modByMonic returns a canonical polynomial when p is canonical.

theorem CompPoly.CPolynomial.Raw.subScaledShift_is_trimmed {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (p q : Raw R) (scale : R) (shift : ℕ) : (p.subScaledShift q scale shift).trim = p.subScaledShift q scale shift

subScaledShift ends with .trim, so its result is canonical.

theorem CompPoly.CPolynomial.Raw.modByMonicRemainderOnly_go_canonical {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (n : ℕ) (p q : Raw R) : p.trim = p → (modByMonicRemainderOnly.go n p q).trim = modByMonicRemainderOnly.go n p q

The remainder-only long-division recursion preserves canonicality of p.

theorem CompPoly.CPolynomial.Raw.modByMonicRemainderOnly_canonical {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] {p : Raw R} (hp : p.trim = p) (q : Raw R) : (p.modByMonicRemainderOnly q).trim = p.modByMonicRemainderOnly q

Raw.modByMonicRemainderOnly returns a canonical polynomial when p is canonical.

theorem CompPoly.CPolynomial.Raw.modByMonicByReversal_canonical {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (M : MulLowContext R) {p : Raw R} (hp : p.trim = p) (q : Raw R) : (modByMonicByReversal M p q).trim = modByMonicByReversal M p q

Raw.modByMonicByReversal returns a canonical polynomial when p is canonical. Either branch ends in a result whose trim is itself: the reversal branch ends with Raw.sub (which trims), and the fallback uses modByMonicRemainderOnly.

theorem CompPoly.CPolynomial.Raw.div_canonical {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (p q : Raw R) : (p.div q).trim = p.div q

Raw.div returns a canonical polynomial (no condition on inputs).

theorem CompPoly.CPolynomial.Raw.mod_canonical {R : Type u_1} [BEq R] [Field R] [LawfulBEq R] (p q : Raw R) : (p.mod q).trim = p.mod q

Raw.mod returns a canonical polynomial (no condition on inputs). The intermediate C (q.leadingCoeff)⁻¹ • p is C _ * p via Mul.toSMul, which trims.

@[implicit_reducible]

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

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

pow preserves trimming (Raw-level version).

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

Additive law for exponentiation: $ p ^ {a + b} = p ^ a \cdot p ^ b $.

theorem CompPoly.CPolynomial.Raw.mul_trim_eq_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a b : Raw R) : a.trim * b.trim = a * b

Multiplication depends only on the coefficient sequences of its inputs, so trimming either side preserves the product.

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

powBySq agrees with pow (repeated squaring = repeated multiplication).

powBySq accumulates intermediate squarings with the untrimmed mulRaw and trims once at the end, so the proof bridges through mul_trim_eq_mul to relate each mulRaw step back to the spec pow.