Documentation

CompPoly.Univariate.ToPoly.Impl

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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