HexMvPolyTheory.Kernel

source

@[reducible, inline]

abbrev HexMvPolyTheory.Kernel.Term (κ : Type u_1) :

Type u_1

Equations

HexMvPolyTheory.Kernel.Term = Hex.MvPoly.Kernel.Term

Instances For

source

@[reducible, inline]

abbrev HexMvPolyTheory.Kernel.PolyList (κ : Type u_1) :

Type u_1

Equations

HexMvPolyTheory.Kernel.PolyList = Hex.MvPoly.Kernel.PolyList

Instances For

source

noncomputable def HexMvPolyTheory.Kernel.denote {n : ℕ} {R : Type u} [CommSemiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p : PolyList R) :

MvPolynomial (Fin n) R

Denote a kernel term list as a Mathlib multivariate polynomial.

Equations

HexMvPolyTheory.Kernel.denote p = HexMvPolyTheory.equiv (Hex.MvPoly.Kernel.denote p)

Instances For

source

theorem HexMvPolyTheory.Kernel.denote_one {n : ℕ} {R : Type u} [CommSemiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] :

denote (Hex.MvPoly.Kernel.one n) = 1

The list multiplicative identity denotes the Mathlib identity.

source

theorem HexMvPolyTheory.Kernel.denote_add {n : ℕ} {R : Type u} [CommSemiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p q : PolyList R) :

denote (Hex.MvPoly.Kernel.add p q) = denote p + denote q

List addition has the same denotation as Mathlib addition.

source

theorem HexMvPolyTheory.Kernel.denote_mul {n : ℕ} {R : Type u} [CommSemiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p q : PolyList R) (hp : ∀ t ∈ p, t.1.length = n) (hq : ∀ t ∈ q, t.1.length = n) :

denote (Hex.MvPoly.Kernel.mul p q) = denote p * denote q

List multiplication has the same denotation as Mathlib multiplication.

source

theorem HexMvPolyTheory.Kernel.denote_neg {n : ℕ} {R : Type u} [CommRing R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p : PolyList R) :

denote (Hex.MvPoly.Kernel.neg p) = -denote p

List negation has the same denotation as Mathlib negation.

source

theorem HexMvPolyTheory.Kernel.denote_sub {n : ℕ} {R : Type u} [CommRing R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p q : PolyList R) :

denote (Hex.MvPoly.Kernel.sub p q) = denote p - denote q

List subtraction has the same denotation as Mathlib subtraction.

source

theorem HexMvPolyTheory.Kernel.denote_smul {n : ℕ} {R : Type u} [CommSemiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (a : R) (p : PolyList R) :

denote (Hex.MvPoly.Kernel.smul a p) = MvPolynomial.C a * denote p

List scalar multiplication denotes multiplication by a Mathlib constant.

source

theorem HexMvPolyTheory.Kernel.denote_toList {n : ℕ} {R : Type u} [CommSemiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (p : Hex.MvPoly n R cmp) :

denote (Hex.MvPoly.Kernel.toList p) = equiv p

Producer conversion reads as the corresponding Mathlib polynomial.

source

theorem HexMvPolyTheory.Kernel.isZero_iff {n : ℕ} {R : Type u} [CommSemiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {p : PolyList R} (hp : Hex.MvPoly.Kernel.Canonical n p) :

Hex.MvPoly.Kernel.isZero p = true ↔ denote p = 0

The list zero test agrees with zero Mathlib denotation on canonical inputs.

source

theorem HexMvPolyTheory.Kernel.beq_iff {n : ℕ} {R : Type u} [CommSemiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {p q : PolyList R} (hp : Hex.MvPoly.Kernel.Canonical n p) (hq : Hex.MvPoly.Kernel.Canonical n q) :

Hex.MvPoly.Kernel.beq p q = true ↔ denote p = denote q

The list equality test agrees with equality of Mathlib denotations on canonical inputs.