Documentation

CompPoly.Univariate.ToPoly.Core

Computable Univariate To Polynomial #

Conversions between computable univariate polynomials and mathlib Polynomial.

source
def Polynomial.toImpl {R : Type u_1} [Semiring R] (p : Polynomial R) :
CompPoly.CPolynomial.Raw R

Convert a mathlib Polynomial to a CPolynomial.Raw by extracting coefficients up to the degree.

Instances For
    source
    noncomputable def CompPoly.CPolynomial.Raw.toPoly {R : Type u_1} [Semiring R] (p : Raw R) :
    Polynomial R

    Convert a CPolynomial.Raw to a (mathlib) Polynomial.

    Instances For
      source
      noncomputable def CompPoly.CPolynomial.Raw.toPoly' {R : Type u_1} [Semiring R] (p : Raw R) :
      Polynomial R

      Alternative definition of toPoly using Finsupp; currently unused.

      Instances For
        source
        noncomputable def CompPoly.CPolynomial.toPoly {R : Type u_1} [Zero R] [Semiring R] (p : CPolynomial R) :
        Polynomial R

        Convert a canonical polynomial to a (mathlib) Polynomial.

        Instances For
          source
          def CompPoly.CPolynomial.Raw.ofPoly {R : Type u_1} [Semiring R] (p : Polynomial R) :
          Raw R

          Alias of Polynomial.toImpl.

          Convert a mathlib Polynomial to a CPolynomial.Raw by extracting coefficients up to the degree.

          Instances For
            source
            theorem CompPoly.CPolynomial.Raw.eval_toPoly_eq_eval {Q : Type u_2} [Semiring Q] (x : Q) (p : Raw Q) :
            Polynomial.eval x p.toPoly = eval x p

            Evaluation is preserved by toPoly.

            source
            theorem CompPoly.CPolynomial.Raw.coeff_toPoly {Q : Type u_2} [Semiring Q] {p : Raw Q} {n : ℕ} :
            p.toPoly.coeff n = p.coeff n

            The coefficients of p.toPoly match those of p.

            source
            theorem CompPoly.CPolynomial.Raw.toImpl_elim {Q : Type u_2} [Semiring Q] (p : Polynomial Q) :
            p = 0 ∧ p.toImpl = #[] ∨ p ≠ 0 ∧ p.toImpl = Array.ofFn fun (i : Fin (p.natDegree + 1)) => p.coeff ↑i

            Case analysis for toImpl: either the polynomial is zero or has a specific form.

            source
            theorem CompPoly.CPolynomial.Raw.toPoly_toImpl {Q : Type u_2} [Semiring Q] {p : Polynomial Q} :
            p.toImpl.toPoly = p

            toImpl is a right-inverse of toPoly: the round-trip from Polynomial is the identity.

            This shows toPoly is surjective and toImpl is injective.

            source
            theorem CompPoly.CPolynomial.Raw.toPoly_trim {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] {p : Raw R} :
            p.trim.toPoly = p.toPoly

            Trimming doesn't change the toPoly image.

            source
            theorem CompPoly.CPolynomial.Raw.toPoly_addRaw {Q : Type u_2} [Semiring Q] {p q : Raw Q} :
            (p.addRaw q).toPoly = p.toPoly + q.toPoly

            toPoly preserves addition.

            source
            theorem CompPoly.CPolynomial.Raw.toPoly_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) :
            (p + q).toPoly = p.toPoly + q.toPoly
            source
            theorem CompPoly.CPolynomial.Raw.toImpl_nonzero {Q : Type u_2} [Semiring Q] {p : Polynomial Q} (hp : p ≠ 0) :
            Array.size p.toImpl > 0

            Non-zero polynomials map to non-empty arrays.

            source
            theorem CompPoly.CPolynomial.Raw.getLast_toImpl {Q : Type u_2} [Semiring Q] {p : Polynomial Q} (hp : p ≠ 0) :
            have h := ⋯; p.toImpl[Array.size p.toImpl - 1] = p.leadingCoeff

            The last coefficient of toImpl p is the leading coefficient of p.

            source
            @[simp]
            theorem CompPoly.CPolynomial.Raw.isCanonical_toImpl {R : Type u_1} [Semiring R] (p : Polynomial R) :
            p.toImpl.IsCanonical

            toImpl lands in the semantic canonical carrier used by CPolynomial.

            source
            @[simp]
            theorem CompPoly.CPolynomial.Raw.trim_toImpl {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Polynomial R) :
            p.toImpl.trim = p.toImpl

            toImpl produces canonical polynomials (no trailing zeros).

            source
            theorem CompPoly.CPolynomial.toImpl_toPoly_of_canonical {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) :
            p.toPoly.toImpl = ↑p

            On canonical polynomials, toImpl is a left-inverse of toPoly.

            This shows toPoly is a bijection from CPolynomial R to Polynomial R.

            source
            @[simp]
            theorem CompPoly.CPolynomial.Raw.toImpl_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) :
            p.toPoly.toImpl = p.trim

            The round-trip from CPolynomial.Raw to Polynomial and back yields the canonical form.

            source
            theorem CompPoly.CPolynomial.toPoly_eq_zero_iff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) :
            p.toPoly = 0 ↔ p = 0

            toPoly maps a canonical polynomial to 0 iff the polynomial is 0.

            source
            @[simp]
            theorem CompPoly.CPolynomial.eval_toImpl_eq_eval {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (x : R) (p : Polynomial R) :
            Raw.eval x p.toImpl = Polynomial.eval x p

            Evaluation is preserved by toImpl.

            source
            @[simp]
            theorem CompPoly.CPolynomial.Raw.eval_trim_eq_eval {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (x : R) (p : Raw R) :
            eval x p.trim = eval x p

            Evaluation is unchanged by trimming.