noncomputable def HexPolyFpMathlib.fpPolyToPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : Polynomial (ZMod p)

Interpret an executable FpPoly p as a Mathlib polynomial over ZMod p.

Equations

• HexPolyFpMathlib.fpPolyToPolynomial f = ∑ i ∈ Finset.range (Hex.DensePoly.size f), (Polynomial.monomial i) (HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff f i))

def HexPolyFpMathlib.polynomialToFpPoly {p : ℕ} [Hex.ZMod64.Bounds p] (f : Polynomial (ZMod p)) : Hex.FpPoly p

Rebuild an executable FpPoly p from a Mathlib polynomial over ZMod p.

Equations

• HexPolyFpMathlib.polynomialToFpPoly f = Hex.DensePoly.ofList (List.map (fun (i : ℕ) => HexModArithMathlib.ZMod64.equiv.symm (f.coeff i)) (List.range (f.natDegree + 1)))

theorem HexPolyFpMathlib.coeff_fpPolyToPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) (n : ℕ) : (fpPolyToPolynomial f).coeff n = HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff f n)

Coefficient view of the direct finite-field transport fpPolyToPolynomial, the standalone form of coeff_toMathlibPolynomial available before the ring equivalence is assembled.

noncomputable def HexPolyFpMathlib.fpPolyEquiv {p : ℕ} [Hex.ZMod64.Bounds p] : Hex.FpPoly p ≃+* Polynomial (ZMod p)

The executable finite-field polynomial representation is ring-equivalent to Mathlib polynomials over ZMod p.

Equations

• HexPolyFpMathlib.fpPolyEquiv = { toFun := HexPolyFpMathlib.fpPolyToPolynomial, invFun := HexPolyFpMathlib.polynomialToFpPoly, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

noncomputable def HexPolyFpMathlib.toMathlibPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : Polynomial (ZMod p)

Interpret an executable FpPoly p as a Mathlib polynomial over ZMod p.

Equations

• HexPolyFpMathlib.toMathlibPolynomial f = HexPolyFpMathlib.fpPolyEquiv f

@[simp]

theorem HexPolyFpMathlib.fpPolyEquiv_apply {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : fpPolyEquiv f = toMathlibPolynomial f

Applying the ring equivalence is the forward transport. The named forward map is the normal form: statements about an executable polynomial's Mathlib image read better without a RingEquiv coercion in the way.

@[simp]

theorem HexPolyFpMathlib.fpPolyEquiv_symm_apply {p : ℕ} [Hex.ZMod64.Bounds p] (f : Polynomial (ZMod p)) : fpPolyEquiv.symm f = polynomialToFpPoly f

Applying the inverse of the ring equivalence is polynomialToFpPoly, the partner of HexPolyFpMathlib.fpPolyEquiv_apply for the backward direction.

@[simp]

theorem HexPolyFpMathlib.coeff_toMathlibPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) (n : ℕ) : (toMathlibPolynomial f).coeff n = HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff f n)

Coefficients are preserved by the equivalence with Mathlib polynomials.

@[simp]

theorem HexPolyFpMathlib.coeff_polynomialToFpPoly {p : ℕ} [Hex.ZMod64.Bounds p] (f : Polynomial (ZMod p)) (n : ℕ) : Hex.DensePoly.coeff (polynomialToFpPoly f) n = HexModArithMathlib.ZMod64.ofZMod (f.coeff n)

Rebuilding a Mathlib polynomial preserves coefficients, transported back through the ZMod64 equivalence.

theorem HexPolyFpMathlib.toMathlibPolynomial_monic {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : Hex.DensePoly.Monic f → (toMathlibPolynomial f).Monic

Monicity of executable finite-field polynomials transfers to Mathlib.

No nontriviality hypothesis is required: when ZMod p is trivial every polynomial is monic, and otherwise the executable leading coefficient 1 transports to the Mathlib leading coefficient 1.

@[simp]

theorem HexPolyFpMathlib.natDegree_toMathlibPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : (toMathlibPolynomial f).natDegree = Hex.DensePoly.natDegree f

The executable degree transports to Mathlib's natDegree, with the zero polynomial mapping to degree 0. No nontriviality hypothesis is needed: in the trivial ring every transported polynomial is zero and every executable coefficient is zero as well.

@[simp]

theorem HexPolyFpMathlib.leadingCoeff_toMathlibPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : (toMathlibPolynomial f).leadingCoeff = HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.leadingCoeff f)

The executable leading coefficient transports through toZMod to Mathlib's leading coefficient.

theorem HexPolyFpMathlib.toMathlibPolynomial_derivative {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : toMathlibPolynomial (Hex.DensePoly.derivative f) = Polynomial.derivative (toMathlibPolynomial f)

Formal derivatives commute with the finite-field polynomial transport.

theorem HexPolyFpMathlib.toMathlibPolynomial_mul {p : ℕ} [Hex.ZMod64.Bounds p] (f g : Hex.FpPoly p) : toMathlibPolynomial (f * g) = toMathlibPolynomial f * toMathlibPolynomial g

Multiplication commutes with the finite-field polynomial transport.

theorem HexPolyFpMathlib.toMathlibPolynomial_add {p : ℕ} [Hex.ZMod64.Bounds p] (f g : Hex.FpPoly p) : toMathlibPolynomial (f + g) = toMathlibPolynomial f + toMathlibPolynomial g

Addition commutes with the finite-field polynomial transport.

theorem HexPolyFpMathlib.toMathlibPolynomial_sub {p : ℕ} [Hex.ZMod64.Bounds p] (f g : Hex.FpPoly p) : toMathlibPolynomial (f - g) = toMathlibPolynomial f - toMathlibPolynomial g

Subtraction commutes with the finite-field polynomial transport.

@[simp]

theorem HexPolyFpMathlib.toMathlibPolynomial_neg {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) : toMathlibPolynomial (-f) = -toMathlibPolynomial f

Negation commutes with the finite-field polynomial transport.

theorem HexPolyFpMathlib.toMathlibPolynomial_C {p : ℕ} [Hex.ZMod64.Bounds p] (c : Hex.ZMod64 p) : toMathlibPolynomial (Hex.DensePoly.C c) = Polynomial.C (HexModArithMathlib.ZMod64.toZMod c)

The constant executable polynomial transports to the Mathlib constant.

@[simp]

theorem HexPolyFpMathlib.toMathlibPolynomial_monomial {p : ℕ} [Hex.ZMod64.Bounds p] (m : ℕ) (c : Hex.ZMod64 p) : toMathlibPolynomial (Hex.DensePoly.monomial m c) = (Polynomial.monomial m) (HexModArithMathlib.ZMod64.toZMod c)

An executable monomial transports to the corresponding Mathlib monomial.

@[simp]

theorem HexPolyFpMathlib.toMathlibPolynomial_monomial_one {p : ℕ} [Hex.ZMod64.Bounds p] (m : ℕ) : toMathlibPolynomial (Hex.DensePoly.monomial m 1) = Polynomial.X ^ m

The monic monomial X^m transports to X^m over ZMod p.

theorem HexPolyFpMathlib.toMathlibPolynomial_X {p : ℕ} [Hex.ZMod64.Bounds p] : toMathlibPolynomial Hex.FpPoly.X = Polynomial.X

The executable indeterminate transports to Mathlib's X.

theorem HexPolyFpMathlib.toMathlibPolynomial_dvd {p : ℕ} [Hex.ZMod64.Bounds p] {f g : Hex.FpPoly p} (h : f ∣ g) : toMathlibPolynomial f ∣ toMathlibPolynomial g

Divisibility transports along the finite-field polynomial map.

theorem HexPolyFpMathlib.toMathlibPolynomial_dvd_iff {p : ℕ} [Hex.ZMod64.Bounds p] {f g : Hex.FpPoly p} : toMathlibPolynomial f ∣ toMathlibPolynomial g ↔ f ∣ g

Executable finite-field polynomials divide one another exactly when their Mathlib images do.

theorem HexPolyFpMathlib.eval₂_toMathlibPolynomial {p : ℕ} [Hex.ZMod64.Bounds p] {S : Type u_1} [Semiring S] (h : ZMod p →+* S) (f : Hex.FpPoly p) (x : S) : Polynomial.eval₂ h x (toMathlibPolynomial f) = ∑ i ∈ Finset.range (Hex.DensePoly.size f), h (HexModArithMathlib.ZMod64.toZMod (Hex.DensePoly.coeff f i)) * x ^ i

Evaluation of a transported polynomial is its degree-indexed coefficient sum after transporting each executable coefficient through toZMod.

theorem HexPolyFpMathlib.primeModulus_of_fact (p : ℕ) [Fact (Nat.Prime p)] : Hex.ZMod64.PrimeModulus p

The Mathlib primality fact yields the executable prime-modulus witness, so executable field-dependent lemmas (gcd/Bezout, modular division) become available in the Mathlib transport layer.

@[instance_reducible]

instance HexPolyFpMathlib.commRing {p : ℕ} [Hex.ZMod64.Bounds p] : CommRing (Hex.FpPoly p)

The executable prime-field polynomials are a Mathlib commutative ring, with the executable operations. Built from the laws HexPolyFp.Ring proves rather than transported along HexPolyFpMathlib.fpPolyEquiv, which would attach the right laws to Mathlib's operations instead of these.

sub and neg are pinned to the executable ones rather than left at the minimal-axioms defaults (a - b = a + -b). HexPolyFp already defines Sub and Neg, so leaving the defaults would put two different subtractions on the type and Mathlib's lemmas would not fire on the spelling callers write.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HexPolyFpMathlib.toMathlibPolynomial_zero {p : ℕ} [Hex.ZMod64.Bounds p] : toMathlibPolynomial 0 = 0

The executable zero polynomial transports to Mathlib's zero polynomial.

@[simp]

theorem HexPolyFpMathlib.toMathlibPolynomial_one {p : ℕ} [Hex.ZMod64.Bounds p] : toMathlibPolynomial 1 = 1

The executable unit polynomial transports to Mathlib's unit polynomial.

@[simp]

theorem HexPolyFpMathlib.toMathlibPolynomial_pow {p : ℕ} [Hex.ZMod64.Bounds p] (f : Hex.FpPoly p) (n : ℕ) : toMathlibPolynomial (f ^ n) = toMathlibPolynomial f ^ n

Powers commute with the finite-field polynomial transport.

@[simp]

theorem HexPolyFpMathlib.polynomialToFpPoly_zero {p : ℕ} [Hex.ZMod64.Bounds p] : polynomialToFpPoly 0 = 0

The inverse transport sends Mathlib's zero polynomial to executable zero.

@[simp]

theorem HexPolyFpMathlib.polynomialToFpPoly_one {p : ℕ} [Hex.ZMod64.Bounds p] : polynomialToFpPoly 1 = 1

The inverse transport sends Mathlib's one polynomial to executable one.

@[simp]

theorem HexPolyFpMathlib.polynomialToFpPoly_C {p : ℕ} [Hex.ZMod64.Bounds p] (c : ZMod p) : polynomialToFpPoly (Polynomial.C c) = Hex.DensePoly.C (HexModArithMathlib.ZMod64.ofZMod c)

The inverse transport sends a Mathlib constant to the corresponding executable constant.

@[simp]

theorem HexPolyFpMathlib.polynomialToFpPoly_neg {p : ℕ} [Hex.ZMod64.Bounds p] (f : Polynomial (ZMod p)) : polynomialToFpPoly (-f) = -polynomialToFpPoly f

The inverse transport commutes with polynomial negation.

@[simp]

theorem HexPolyFpMathlib.polynomialToFpPoly_sub {p : ℕ} [Hex.ZMod64.Bounds p] (f g : Polynomial (ZMod p)) : polynomialToFpPoly (f - g) = polynomialToFpPoly f - polynomialToFpPoly g

The inverse transport commutes with polynomial subtraction.

@[simp]

theorem HexPolyFpMathlib.polynomialToFpPoly_add {p : ℕ} [Hex.ZMod64.Bounds p] (f g : Polynomial (ZMod p)) : polynomialToFpPoly (f + g) = polynomialToFpPoly f + polynomialToFpPoly g

The inverse transport commutes with polynomial addition.

@[simp]

theorem HexPolyFpMathlib.polynomialToFpPoly_mul {p : ℕ} [Hex.ZMod64.Bounds p] (f g : Polynomial (ZMod p)) : polynomialToFpPoly (f * g) = polynomialToFpPoly f * polynomialToFpPoly g

The inverse transport commutes with polynomial multiplication.

@[simp]

theorem HexPolyFpMathlib.polynomialToFpPoly_monomial {p : ℕ} [Hex.ZMod64.Bounds p] (n : ℕ) (c : ZMod p) : polynomialToFpPoly ((Polynomial.monomial n) c) = Hex.DensePoly.monomial n (HexModArithMathlib.ZMod64.ofZMod c)

The inverse transport sends a Mathlib monomial to the corresponding executable monomial.

@[simp]

theorem HexPolyFpMathlib.toMathlibPolynomial_compose {p : ℕ} [Hex.ZMod64.Bounds p] (f g : Hex.FpPoly p) : toMathlibPolynomial (Hex.DensePoly.compose f g) = (toMathlibPolynomial f).comp (toMathlibPolynomial g)

The finite-field transport intertwines executable Horner composition with Mathlib polynomial composition.

theorem HexPolyFpMathlib.linearPow_eq_pow {p : ℕ} [Hex.ZMod64.Bounds p] (b : Hex.FpPoly p) (k : ℕ) : b.linearPow k = b ^ k

The executable linear power is Mathlib's monoid power. HexPolyFp defines linearPow by structural recursion for kernel reduction; the CommRing above supplies npowRec. They agree, and saying so once lets map_pow be used on executable powers.