theorem HexPolyMathlib.list_getD_map_range_zero {R : Type u} [Zero R] (size n : ℕ) (f : ℕ → R) : (List.map f (List.range size)).getD n Zero.zero = if n < size then f n else Zero.zero

Reading a mapped List.range with default zero returns the mapped index inside the range and zero outside it. This is the coefficient-array lookup fact used by coeff_ofPolynomial when rebuilding dense polynomials from Mathlib coefficients.

noncomputable def HexPolyMathlib.toPolynomial {R : Type u} [Semiring R] [DecidableEq R] (p : Hex.DensePoly R) : Polynomial R

Interpret a normalized dense coefficient array as a Mathlib polynomial.

Equations

• HexPolyMathlib.toPolynomial p = ∑ i ∈ Finset.range p.size, (Polynomial.monomial i) (p.coeff i)

def HexPolyMathlib.ofPolynomial {R : Type u} [Semiring R] [DecidableEq R] (p : Polynomial R) : Hex.DensePoly R

Rebuild a normalized dense polynomial from the coefficients of a Mathlib polynomial.

Equations

• HexPolyMathlib.ofPolynomial p = Hex.DensePoly.ofList (List.map p.coeff (List.range (p.natDegree + 1)))

@[simp]

theorem HexPolyMathlib.coeff_ofPolynomial {R : Type u} [Semiring R] [DecidableEq R] (p : Polynomial R) (n : ℕ) : (ofPolynomial p).coeff n = p.coeff n

Rebuilding via ofPolynomial preserves coefficients: the nth coefficient of ofPolynomial p agrees with the nth coefficient of p.

@[simp]

theorem HexPolyMathlib.coeff_toPolynomial {R : Type u} [Semiring R] [DecidableEq R] (p : Hex.DensePoly R) (n : ℕ) : (toPolynomial p).coeff n = p.coeff n

Converting via toPolynomial preserves coefficients: the nth coefficient of toPolynomial p agrees with the nth coefficient of the dense polynomial p.

theorem HexPolyMathlib.eval₂_toPolynomial {R : Type u} {S : Type u_1} [Semiring R] [DecidableEq R] [Semiring S] (f : R →+* S) (p : Hex.DensePoly R) (x : S) : Polynomial.eval₂ f x (toPolynomial p) = ∑ i ∈ Finset.range p.size, f (p.coeff i) * x ^ i

Coefficient-sum evaluation correspondence: evaluating toPolynomial p through a ring hom f at x is the degree-indexed sum ∑ f (p.coeff i) * x ^ i. For a literal ofCoeffs array this unfolds via Finset.sum_range_succ into an explicit polynomial in x, which ring/norm_num can then discharge.

@[simp]

theorem HexPolyMathlib.ofPolynomial_zero {R : Type u} [Semiring R] [DecidableEq R] : ofPolynomial 0 = 0

ofPolynomial sends Mathlib's zero polynomial to the executable zero.

@[simp]

theorem HexPolyMathlib.ofPolynomial_one {R : Type u} [Semiring R] [DecidableEq R] : ofPolynomial 1 = 1

ofPolynomial sends Mathlib's polynomial 1 to the executable constant 1.

@[simp]

theorem HexPolyMathlib.ofPolynomial_C {R : Type u} [Semiring R] [DecidableEq R] (c : R) : ofPolynomial (Polynomial.C c) = Hex.DensePoly.C c

ofPolynomial sends Mathlib's polynomial constant to the executable constant.

@[simp]

theorem HexPolyMathlib.ofPolynomial_neg {R : Type u} [Ring R] [DecidableEq R] (p : Polynomial R) : ofPolynomial (-p) = -ofPolynomial p

ofPolynomial commutes with polynomial negation.

@[simp]

theorem HexPolyMathlib.ofPolynomial_sub {R : Type u} [Ring R] [DecidableEq R] (p q : Polynomial R) : ofPolynomial (p - q) = ofPolynomial p - ofPolynomial q

ofPolynomial commutes with polynomial subtraction.

@[simp]

theorem HexPolyMathlib.ofPolynomial_add {R : Type u} [Semiring R] [DecidableEq R] (p q : Polynomial R) : ofPolynomial (p + q) = ofPolynomial p + ofPolynomial q

ofPolynomial commutes with polynomial addition.

@[simp]

theorem HexPolyMathlib.ofPolynomial_monomial {R : Type u} [Semiring R] [DecidableEq R] (n : ℕ) (c : R) : ofPolynomial ((Polynomial.monomial n) c) = Hex.DensePoly.monomial n c

ofPolynomial sends Mathlib's monomial to the executable monomial.

@[simp]

theorem HexPolyMathlib.toPolynomial_zero {R : Type u} [Semiring R] [DecidableEq R] : toPolynomial 0 = 0

toPolynomial sends the executable zero to Mathlib's zero polynomial.

@[simp]

theorem HexPolyMathlib.toPolynomial_C {R : Type u} [Semiring R] [DecidableEq R] (c : R) : toPolynomial (Hex.DensePoly.C c) = Polynomial.C c

toPolynomial sends the executable constant to Mathlib's polynomial constant.

@[simp]

theorem HexPolyMathlib.toPolynomial_one {R : Type u} [Semiring R] [DecidableEq R] : toPolynomial 1 = 1

toPolynomial sends the executable constant 1 to Mathlib's polynomial 1.

@[simp]

theorem HexPolyMathlib.toPolynomial_ofCoeffs {R : Type u} [Semiring R] [DecidableEq R] (cs : Array R) : toPolynomial (Hex.DensePoly.ofCoeffs cs) = ∑ i ∈ Finset.range cs.size, Polynomial.C (cs.getD i Zero.zero) * Polynomial.X ^ i

toPolynomial reads a raw coefficient array off as the obvious sum, ascending. This is what makes a concrete #p[...] literal readable on the Mathlib side: with Finset.sum_range_succ to expand the range, toPolynomial #p[1, 1, 1] becomes C 1 * X ^ 0 + C 1 * X ^ 1 + C 1 * X ^ 2.

Stated with C _ * X ^ i rather than monomial i _ because that is the form a reader writes a polynomial in, so a use site needs no C_mul_X_pow_eq_monomial rewrite of its own.

@[simp]

theorem HexPolyMathlib.toPolynomial_scale {R : Type u} [Semiring R] [DecidableEq R] (c : R) (p : Hex.DensePoly R) : toPolynomial (Hex.DensePoly.scale c p) = Polynomial.C c * toPolynomial p

toPolynomial sends executable coefficient scaling to multiplication by the corresponding constant polynomial.

@[simp]

theorem HexPolyMathlib.toPolynomial_monomial {R : Type u} [Semiring R] [DecidableEq R] (n : ℕ) (c : R) : toPolynomial (Hex.DensePoly.monomial n c) = (Polynomial.monomial n) c

toPolynomial sends the executable monomial to Mathlib's monomial.

@[simp]

theorem HexPolyMathlib.toPolynomial_add {R : Type u} [Semiring R] [DecidableEq R] (p q : Hex.DensePoly R) : toPolynomial (p + q) = toPolynomial p + toPolynomial q

HexPolyMathlib.toPolynomial commutes with polynomial addition.

@[simp]

theorem HexPolyMathlib.toPolynomial_neg {R : Type u} [Ring R] [DecidableEq R] (p : Hex.DensePoly R) : toPolynomial (-p) = -toPolynomial p

toPolynomial commutes with executable polynomial negation.

@[simp]

theorem HexPolyMathlib.toPolynomial_sub {R : Type u} [Ring R] [DecidableEq R] (p q : Hex.DensePoly R) : toPolynomial (p - q) = toPolynomial p - toPolynomial q

toPolynomial commutes with executable polynomial subtraction.

@[simp]

theorem HexPolyMathlib.toPolynomial_mul {R : Type u} [Semiring R] [DecidableEq R] (p q : Hex.DensePoly R) : toPolynomial (p * q) = toPolynomial p * toPolynomial q

HexPolyMathlib.toPolynomial commutes with polynomial multiplication.

@[simp]

theorem HexPolyMathlib.toPolynomial_derivative {R : Type u} [CommSemiring R] [DecidableEq R] (p : Hex.DensePoly R) : toPolynomial p.derivative = Polynomial.derivative (toPolynomial p)

HexPolyMathlib.toPolynomial intertwines the executable derivative with Mathlib's polynomial derivative.

@[simp]

theorem HexPolyMathlib.toPolynomial_ofPolynomial {R : Type u} [Semiring R] [DecidableEq R] (p : Polynomial R) : toPolynomial (ofPolynomial p) = p

Converting a Mathlib polynomial into the executable representation and back recovers the original: HexPolyMathlib.toPolynomial is a left inverse of HexPolyMathlib.ofPolynomial.

@[simp]

theorem HexPolyMathlib.ofPolynomial_toPolynomial {R : Type u} [Semiring R] [DecidableEq R] (p : Hex.DensePoly R) : ofPolynomial (toPolynomial p) = p

Converting an executable polynomial into a Mathlib polynomial and back recovers the original: HexPolyMathlib.ofPolynomial is a left inverse of HexPolyMathlib.toPolynomial.

noncomputable def HexPolyMathlib.equiv {R : Type u} [Semiring R] [DecidableEq R] : Hex.DensePoly R ≃+* Polynomial R

The executable dense-polynomial representation is ring-equivalent to Mathlib polynomials.

Equations

• HexPolyMathlib.equiv = { toFun := HexPolyMathlib.toPolynomial, invFun := HexPolyMathlib.ofPolynomial, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem HexPolyMathlib.equiv_apply {R : Type u} [Semiring R] [DecidableEq R] (p : Hex.DensePoly R) : equiv p = toPolynomial p

The ring isomorphism equiv is computed by toPolynomial in the forward direction.

@[simp]

theorem HexPolyMathlib.equiv_symm_apply {R : Type u} [Semiring R] [DecidableEq R] (p : Polynomial R) : equiv.symm p = ofPolynomial p

The inverse of the ring isomorphism equiv is computed by ofPolynomial.

noncomputable def HexPolyMathlib.mapEquiv {R : Type u} {S : Type v} [Semiring R] [DecidableEq R] [Semiring S] [DecidableEq S] (e : R ≃+* S) : Hex.DensePoly R ≃+* Hex.DensePoly S

Apply a coefficient-ring equivalence to a dense polynomial.

Equations

• HexPolyMathlib.mapEquiv e = HexPolyMathlib.equiv.trans ((Polynomial.mapEquiv e).trans HexPolyMathlib.equiv.symm)

@[simp]

theorem HexPolyMathlib.mapEquiv_apply {R : Type u} {S : Type v} [Semiring R] [DecidableEq R] [Semiring S] [DecidableEq S] (e : R ≃+* S) (p : Hex.DensePoly R) : (mapEquiv e) p = ofPolynomial (Polynomial.map e.toRingHom (toPolynomial p))

@[simp]

theorem HexPolyMathlib.mapEquiv_symm_apply {R : Type u} {S : Type v} [Semiring R] [DecidableEq R] [Semiring S] [DecidableEq S] (e : R ≃+* S) (p : Hex.DensePoly S) : (mapEquiv e).symm p = ofPolynomial (Polynomial.map e.symm.toRingHom (toPolynomial p))

@[simp]

theorem HexPolyMathlib.ofPolynomial_mul {R : Type u} [Semiring R] [DecidableEq R] (p q : Polynomial R) : ofPolynomial (p * q) = ofPolynomial p * ofPolynomial q

ofPolynomial commutes with polynomial multiplication.

@[simp]

theorem HexPolyMathlib.natDegree_toPolynomial {R : Type u} [Semiring R] [DecidableEq R] (p : Hex.DensePoly R) : (toPolynomial p).natDegree = p.degree?.getD 0

HexPolyMathlib.toPolynomial transports the executable degree to Mathlib's natDegree, with the zero polynomial mapping to 0.

@[simp]

theorem HexPolyMathlib.leadingCoeff_toPolynomial {R : Type u} [Semiring R] [DecidableEq R] (p : Hex.DensePoly R) : (toPolynomial p).leadingCoeff = p.leadingCoeff

toPolynomial transports the executable leading coefficient to Mathlib's leadingCoeff.

theorem HexPolyMathlib.toPolynomial_dvd {R : Type u} [Semiring R] [DecidableEq R] {p q : Hex.DensePoly R} (hdvd : p ∣ q) : toPolynomial p ∣ toPolynomial q

toPolynomial preserves divisibility: a divisibility in the executable representation transfers to the corresponding Mathlib polynomials.

theorem HexPolyMathlib.ofPolynomial_dvd {R : Type u} [Semiring R] [DecidableEq R] {p q : Polynomial R} (hdvd : p ∣ q) : ofPolynomial p ∣ ofPolynomial q

ofPolynomial preserves divisibility: a divisibility of Mathlib polynomials transfers to the corresponding executable representations.

theorem HexPolyMathlib.toPolynomial_dvd_iff {R : Type u} [Semiring R] [DecidableEq R] {p q : Hex.DensePoly R} : toPolynomial p ∣ toPolynomial q ↔ p ∣ q

HexPolyMathlib.toPolynomial both preserves and reflects divisibility: executable polynomials divide one another exactly when their Mathlib images do.

@[simp]

theorem HexPolyMathlib.toPolynomial_compose {R : Type u} [CommSemiring R] [DecidableEq R] (p q : Hex.DensePoly R) : toPolynomial (p.compose q) = (toPolynomial p).comp (toPolynomial q)

toPolynomial intertwines the executable Horner composition with Mathlib's polynomial composition.