noncomputable def HexMvPolyTheory.Kernel.residueEquiv (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : Hex.MvPoly n (Hex.ZMod64 p) cmp ≃+* MvPolynomial (Fin n) (ZMod p)

Change both the polynomial representation and its residue coefficient carrier.

Equations

• HexMvPolyTheory.Kernel.residueEquiv p = HexMvPolyTheory.equiv.trans (MvPolynomial.mapEquiv (Fin n) HexModArithTheory.ZMod64.equiv)

noncomputable def HexMvPolyTheory.Kernel.denoteMod (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (a : PolyList ℕ) : MvPolynomial (Fin n) (ZMod p)

Mathlib denotation of the kernel's natural-residue encoding.

Equations

• HexMvPolyTheory.Kernel.denoteMod p a = (HexMvPolyTheory.Kernel.residueEquiv p) (Hex.MvPoly.Kernel.denoteMod p a)

@[simp]

theorem HexMvPolyTheory.Kernel.denoteMod_nil (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : denoteMod p [] = 0

The empty residue list denotes zero in Mathlib.

@[simp]

theorem HexMvPolyTheory.Kernel.denoteMod_oneMod (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : denoteMod p (Hex.MvPoly.Kernel.oneMod p n) = 1

The modular identity denotes the Mathlib polynomial identity.

theorem HexMvPolyTheory.Kernel.denoteMod_addMod (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a b : PolyList ℕ} (ha : Hex.MvPoly.Kernel.CanonicalMod p n a) (hb : Hex.MvPoly.Kernel.CanonicalMod p n b) : denoteMod p (Hex.MvPoly.Kernel.addMod p a b) = denoteMod p a + denoteMod p b

Modular addition denotes Mathlib polynomial addition.

theorem HexMvPolyTheory.Kernel.denoteMod_mulMod (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a b : PolyList ℕ} (ha : Hex.MvPoly.Kernel.CanonicalMod p n a) (hb : Hex.MvPoly.Kernel.CanonicalMod p n b) : denoteMod p (Hex.MvPoly.Kernel.mulMod p a b) = denoteMod p a * denoteMod p b

Modular multiplication denotes Mathlib polynomial multiplication.

theorem HexMvPolyTheory.Kernel.denoteMod_negMod (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a : PolyList ℕ} (ha : Hex.MvPoly.Kernel.CanonicalMod p n a) : denoteMod p (Hex.MvPoly.Kernel.negMod p a) = -denoteMod p a

Modular negation denotes Mathlib polynomial negation.

theorem HexMvPolyTheory.Kernel.denoteMod_subMod (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a b : PolyList ℕ} (ha : Hex.MvPoly.Kernel.CanonicalMod p n a) (hb : Hex.MvPoly.Kernel.CanonicalMod p n b) : denoteMod p (Hex.MvPoly.Kernel.subMod p a b) = denoteMod p a - denoteMod p b

Modular subtraction denotes Mathlib polynomial subtraction.

theorem HexMvPolyTheory.Kernel.residueEquiv_C (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (c : Hex.ZMod64 p) : (residueEquiv p) (Hex.MvPoly.C c) = MvPolynomial.C (HexModArithTheory.ZMod64.equiv c)

Executable constants map to constants over Mathlib residues.

@[simp]

theorem HexMvPolyTheory.Kernel.residueEquiv_monomial (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (m : Hex.Mono n) (c : Hex.ZMod64 p) : (residueEquiv p) (Hex.MvPoly.monomial m c) = (MvPolynomial.monomial (monoEquiv m)) (HexModArithTheory.ZMod64.equiv c)

Residue correspondence preserves each serialized monomial.

theorem HexMvPolyTheory.Kernel.denoteMod_cons (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (e : List ℕ) (c : ℕ) (a : PolyList ℕ) : denoteMod p ((e, c) :: a) = (MvPolynomial.monomial (monoEquiv (Hex.MvPoly.Kernel.mono n e))) ↑c + denoteMod p a

Interpret a serialized residue term followed by the remaining support.

theorem HexMvPolyTheory.Kernel.denoteMod_smulMod (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (c : ℕ) {a : PolyList ℕ} (ha : Hex.MvPoly.Kernel.CanonicalMod p n a) : denoteMod p (Hex.MvPoly.Kernel.smulMod p c a) = MvPolynomial.C ↑c * denoteMod p a

Modular scaling denotes multiplication by the natural scalar in ZMod p.

theorem HexMvPolyTheory.Kernel.isZero_mod_iff (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a : PolyList ℕ} (ha : Hex.MvPoly.Kernel.CanonicalMod p n a) : Hex.MvPoly.Kernel.isZero a = true ↔ denoteMod p a = 0

Canonical residue zero tests are exact in Mathlib.

theorem HexMvPolyTheory.Kernel.beq_mod_iff (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {a b : PolyList ℕ} (ha : Hex.MvPoly.Kernel.CanonicalMod p n a) (hb : Hex.MvPoly.Kernel.CanonicalMod p n b) : Hex.MvPoly.Kernel.beq a b = true ↔ denoteMod p a = denoteMod p b

Canonical residue equality tests are exact in Mathlib.

theorem HexMvPolyTheory.Kernel.denoteMod_ofResidues (p : ℕ) [Hex.ZMod64.Bounds p] {n : ℕ} {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (a : Hex.MvPoly n (Hex.ZMod64 p) cmp) : denoteMod p (Hex.MvPoly.Kernel.ofResidues p (Hex.MvPoly.Kernel.toList a)) = (residueEquiv p) a

The complete producer encoding denotes the corresponding Mathlib polynomial.