Proofs of Correctness for CPolynomial Operations, wrt Mathlib Specs

Proofs that operations defined on CPolynomial and CPolynomial.Raw are correct wrt the mathlib specs, using the ring equivalence

theorem CompPoly.CPolynomial.monomial_toPoly {R : Type u_1} [Semiring R] [DecidableEq R] [LawfulBEq R] (n : ℕ) (c : R) : (monomial n c).toPoly = (Polynomial.monomial n) c

CPolynomial.monomial is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.C_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r : R) : (C r).toPoly = Polynomial.C r

CPolynomial.C is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.X_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : X.toPoly = Polynomial.X

CPolynomial.X is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.eval_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (x : R) (p : CPolynomial R) : eval x p = Polynomial.eval x p.toPoly

CPolynomial.eval is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.eval_C {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (a c : R) : eval a (C c) = c

Evaluation of a constant computable polynomial.

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

Raw.eval₂ is correct wrt the Mathlib spec.

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

CPolynomial.eval₂ is correct wrt the Mathlib spec.

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

CPolynomial.coeff is correct wrt the Mathlib spec.

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

Evaluation at zero returns the constant coefficient.

theorem CompPoly.CPolynomial.divX_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.divX.toPoly = p.toPoly.divX

CPolynomial.divX is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.support_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.support = p.toPoly.support

CPolynomial.support is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.degree_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.degree = p.toPoly.degree

CPolynomial.degree is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.natDegree_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.natDegree = p.toPoly.natDegree

CPolynomial.natDegree is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.leadingCoeff_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.leadingCoeff = p.toPoly.leadingCoeff

CPolynomial.leadingCoeff is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.monic_toPoly_iff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : p.monic = true ↔ p.toPoly.Monic

CPolynomial.monic is correct wrt the Mathlib spec

theorem CompPoly.CPolynomial.erase_toPoly {R : Type u_2} [Ring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (p : CPolynomial R) : (erase n p).toPoly = Polynomial.erase n p.toPoly

CPolynomial.erase is correct wrt the Mathlib spec.

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

CPolynomial.C r mul CPolynomial.X ^ n is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.lcoeff_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (n : ℕ) (p : CPolynomial R) : (lcoeff n) p = (Polynomial.lcoeff R n) p.toPoly

CPolynomial.lcoeff is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.degreeLE_toPoly {R : Type u_1} [Semiring R] {n : WithBot ℕ} [BEq R] [LawfulBEq R] {p : CPolynomial R} : p ∈ degreeLE n ↔ p.toPoly ∈ Polynomial.degreeLE R n

CPolynomial.degreeLE is correct wrt the Mathlib spec.

theorem CompPoly.CPolynomial.degreeLT_toPoly {R : Type u_1} [Semiring R] {n : ℕ} [BEq R] [LawfulBEq R] {p : CPolynomial R} : p ∈ degreeLT n ↔ p.toPoly ∈ Polynomial.degreeLT R n

CPolynomial.degreeLT is correct wrt the Mathlib spec.

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

Evaluation preserves multiplication.

theorem CompPoly.CPolynomial.eval_ext {R : Type u_1} [CommRing R] [DecidableEq R] [BEq R] [LawfulBEq R] [IsDomain R] {p q : CPolynomial R} {d : ℕ} {S : Finset R} (hdeg : (p - q).natDegree ≤ d) (hagree : d < {r ∈ S | eval r p = eval r q}.card) : p = q

Univariate eval-extensionality (degree-bounded). Two CPolynomials over an integral domain that agree on more than $d$ points of a Finset S are equal, when $d$ bounds the natural degree of their difference.

The degree bound is needed over finite fields, where two distinct polynomials may agree on every field element.

theorem CompPoly.CPolynomial.eval_sub {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] (a : R) (p q : CPolynomial R) : eval a (p - q) = eval a p - eval a q

Evaluation preserves subtraction.

theorem CompPoly.CPolynomial.eval_one {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (a : R) : eval a 1 = 1

Evaluation of the constant one computable polynomial.

theorem CompPoly.CPolynomial.eval_divX_eq_zero_of_ne_zero_root {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] {p : CPolynomial R} {a : R} (ha : a ≠ 0) (hcoeff : p.coeff 0 = 0) (hroot : eval a p = 0) : eval a p.divX = 0

Dividing by X preserves a nonzero root when the constant coefficient vanishes.

theorem CompPoly.CPolynomial.divX_ne_zero_of_ne_zero_coeff_zero {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] {p : CPolynomial R} (hp : p ≠ 0) (hcoeff : p.coeff 0 = 0) : p.divX ≠ 0

If a nonzero polynomial has zero constant coefficient, its quotient by X is nonzero.

theorem CompPoly.CPolynomial.Raw.eval_sub_C_mul_X_pow_trim_eq_self_of_eval_eq_zero {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : Raw R) (scale : R) (shift : ℕ) {x : R} (hq : eval x q = 0) : eval x (p - C scale * (q * X ^ shift)).trim = eval x p

theorem CompPoly.CPolynomial.Raw.eval_divModByMonicAux_go_snd_eq_self_of_eval_eq_zero {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (fuel : ℕ) (p q : Raw R) {x : R} : eval x q = 0 → eval x (divModByMonicAux.go fuel p q).2 = eval x p

theorem CompPoly.CPolynomial.Raw.eval_modByMonic_eq_self_of_eval_eq_zero {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : Raw R) {x : R} (hq : eval x q = 0) : eval x (p.modByMonic q) = eval x p

Reducing by a polynomial that vanishes at x preserves evaluation at x.

theorem CompPoly.CPolynomial.eval_modByMonic_eq_self_of_eval_eq_zero {R : Type u_1} [Field R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) {x : R} (hq : eval x q = 0) : eval x (p.modByMonic q) = eval x p

Reducing by a polynomial that vanishes at x preserves evaluation at x.