9.8. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexPolyMathlib connects it to Mathlib: every Hex.DensePoly corresponds to a Mathlib Polynomial with the same coefficients. The two transfer maps go each way.

def

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

Interpret a normalized dense coefficient array as a Mathlib polynomial.

def

HexPolyMathlib.ofPolynomial.{u} {R : Type u} [Semiring R]
  [DecidableEq R] (p : Polynomial R) : Hex.DensePoly R
HexPolyMathlib.ofPolynomial.{u}
  {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.

They are mutually inverse:

theorem

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

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

theorem

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

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

toPolynomial is a degree-preserving ring homomorphism. Addition, multiplication, and the degree transfer:

theorem

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

toPolynomial commutes with polynomial addition.

theorem

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

toPolynomial commutes with polynomial multiplication.

theorem

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

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

The maps and laws bundle into a ring equivalence, and divisibility transfers through it:

def

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

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

theorem

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

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