def HexSparsePolyMathlib.denseEquiv {R : Type u} [CommRing R] [DecidableEq R] : Hex.SparsePoly R ≃+* Hex.DensePoly R

The executable sparse representation is ring-equivalent to the executable dense representation, by the core library's conversions.

Equations

• HexSparsePolyMathlib.denseEquiv = { toFun := Hex.SparsePoly.toDense, invFun := Hex.SparsePoly.ofDense, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem HexSparsePolyMathlib.denseEquiv_apply {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) : denseEquiv s = s.toDense

The ring isomorphism denseEquiv is computed by Hex.SparsePoly.toDense in the forward direction.

@[simp]

theorem HexSparsePolyMathlib.denseEquiv_symm_apply {R : Type u} [CommRing R] [DecidableEq R] (p : Hex.DensePoly R) : denseEquiv.symm p = Hex.SparsePoly.ofDense p

The inverse of denseEquiv is computed by Hex.SparsePoly.ofDense.

noncomputable def HexSparsePolyMathlib.equiv {R : Type u} [CommRing R] [DecidableEq R] : Hex.SparsePoly R ≃+* Polynomial R

The executable sparse representation is ring-equivalent to Mathlib polynomials.

Equations

• HexSparsePolyMathlib.equiv = HexSparsePolyMathlib.denseEquiv.trans HexPolyMathlib.equiv

theorem HexSparsePolyMathlib.equiv_apply {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) : equiv s = HexPolyMathlib.toPolynomial s.toDense

The ring isomorphism equiv is computed by converting to the dense representation and reading it as a Mathlib polynomial. Not simp: the correspondence lemmas below are keyed on equiv s directly, and unfolding first would preempt them.

theorem HexSparsePolyMathlib.equiv_symm_apply {R : Type u} [CommRing R] [DecidableEq R] (p : Polynomial R) : equiv.symm p = Hex.SparsePoly.ofDense (HexPolyMathlib.ofPolynomial p)

The inverse of equiv rebuilds the dense representation and converts it to canonical sparse form.

theorem HexSparsePolyMathlib.equiv_toDense {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) : HexPolyMathlib.equiv s.toDense = equiv s

The two equivalences agree across the dense conversion.

@[simp]

theorem HexSparsePolyMathlib.coeff_equiv {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) (e : ℕ) : (equiv s).coeff e = s.coeff e

equiv preserves coefficients; the identification is exact, coefficient by coefficient.

theorem HexSparsePolyMathlib.equiv_support {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) : (equiv s).support = s.support.toList.toFinset

The stored exponents of the canonical representation are exactly Mathlib's support: the headline sense in which the representation is sparse.

@[simp]

theorem HexSparsePolyMathlib.equiv_eval {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) (x : R) : Polynomial.eval x (equiv s) = s.eval x

Evaluation corresponds: Mathlib evaluation of the image is the executable gap-Horner evaluation.

theorem HexSparsePolyMathlib.equiv_derivative {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) : Polynomial.derivative (equiv s) = equiv s.derivative

Differentiation corresponds: Mathlib's derivative of the image is the image of the executable derivative.

theorem HexSparsePolyMathlib.equiv_compose {R : Type u} [CommRing R] [DecidableEq R] (s t : Hex.SparsePoly R) : (equiv s).comp (equiv t) = equiv (s.compose t)

Composition corresponds: Mathlib's comp of the images is the image of the executable composition.

theorem HexSparsePolyMathlib.equiv_substPow {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) (k : ℕ) : (equiv s).comp (Polynomial.X ^ k) = equiv (s.substPow k)

Exponent substitution corresponds to composition with X ^ k.

theorem HexSparsePolyMathlib.equiv_substScale {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) (a : R) : (equiv s).comp (Polynomial.C a * Polynomial.X) = equiv (s.substScale a)

Argument scaling corresponds to composition with C a * X.

@[simp]

theorem HexSparsePolyMathlib.equiv_monomial {R : Type u} [CommRing R] [DecidableEq R] (e : ℕ) (c : R) : equiv (Hex.SparsePoly.monomial e c) = (Polynomial.monomial e) c

Monomials correspond.

@[simp]

theorem HexSparsePolyMathlib.equiv_C {R : Type u} [CommRing R] [DecidableEq R] (c : R) : equiv (Hex.SparsePoly.C c) = Polynomial.C c

Constants correspond.

@[simp]

theorem HexSparsePolyMathlib.equiv_X {R : Type u} [CommRing R] [DecidableEq R] : equiv Hex.SparsePoly.X = Polynomial.X

The variable corresponds.

@[simp]

theorem HexSparsePolyMathlib.equiv_natDegree {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) : (equiv s).natDegree = s.natDegree

The executable degree corresponds to Mathlib's natDegree, with the zero polynomial mapping to 0.

@[simp]

theorem HexSparsePolyMathlib.equiv_leadingCoeff {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) : (equiv s).leadingCoeff = s.leadingCoeff

The leading coefficient corresponds.

theorem HexSparsePolyMathlib.equiv_monic {R : Type u} [CommRing R] [DecidableEq R] (s : Hex.SparsePoly R) : (equiv s).Monic ↔ s.Monic

Monicity corresponds.