HexMvPoly.Operations

theorem Hex.MvPoly.negCoeff_ne_zero {R : Type u} [Lean.Grind.Ring R] (c : R) (hc : c ≠ 0) :

Negation preserves nonzero coefficients in a ring.

def Hex.MvPoly.add {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Add R] [Zero R] [BEq R] [LawfulBEq R] (p q : MvPoly n R cmp) :

MvPoly n R cmp

Polynomial addition, combining equal monomials and deleting cancellations.

Equations

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

Instances For

source

@[instance_reducible]

instance Hex.MvPoly.instAddOfLawfulBEq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Add R] [Zero R] [BEq R] [LawfulBEq R] :

Add (MvPoly n R cmp)

Equations

Hex.MvPoly.instAddOfLawfulBEq = { add := Hex.MvPoly.add }

source

def Hex.MvPoly.neg {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Neg R] [Zero R] [BEq R] [LawfulBEq R] (p : MvPoly n R cmp) :

MvPoly n R cmp

Coefficientwise negation, filtering any zero result in one tree pass.

Equations

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

Instances For

source

@[instance_reducible]

instance Hex.MvPoly.instNegOfLawfulBEq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Neg R] [Zero R] [BEq R] [LawfulBEq R] :

Neg (MvPoly n R cmp)

Equations

Hex.MvPoly.instNegOfLawfulBEq = { neg := Hex.MvPoly.neg }

source

def Hex.MvPoly.sub {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Add R] [Neg R] [Zero R] [BEq R] [LawfulBEq R] (p q : MvPoly n R cmp) :

MvPoly n R cmp

Polynomial subtraction.

Equations

p.sub q = p.add q.neg

Instances For

source

@[instance_reducible]

instance Hex.MvPoly.instSubOfAddOfNegOfLawfulBEq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Add R] [Neg R] [Zero R] [BEq R] [LawfulBEq R] :

Sub (MvPoly n R cmp)

Equations

Hex.MvPoly.instSubOfAddOfNegOfLawfulBEq = { sub := Hex.MvPoly.sub }

source

def Hex.MvPoly.mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Add R] [Mul R] [Zero R] [BEq R] [LawfulBEq R] (p q : MvPoly n R cmp) :

MvPoly n R cmp

Polynomial multiplication. Every translated product term is accumulated directly into one output map, so collisions and cancellations are normalized as they arise.

Equations

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

Instances For

source

@[instance_reducible]

instance Hex.MvPoly.instMulOfAddOfLawfulBEq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Add R] [Mul R] [Zero R] [BEq R] [LawfulBEq R] :

Mul (MvPoly n R cmp)

Equations

Hex.MvPoly.instMulOfAddOfLawfulBEq = { mul := Hex.MvPoly.mul }

source

def Hex.MvPoly.one {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [One R] [BEq R] [LawfulBEq R] :

MvPoly n R cmp

Multiplicative identity.

Equations

Hex.MvPoly.one = Hex.MvPoly.C 1

Instances For

source

@[instance_reducible]

instance Hex.MvPoly.instOneOfLawfulBEq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Zero R] [One R] [BEq R] [LawfulBEq R] :

One (MvPoly n R cmp)

Equations

Hex.MvPoly.instOneOfLawfulBEq = { one := Hex.MvPoly.one }

source

@[irreducible]

def Hex.MvPoly.npowBySq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Add R] [Mul R] [Zero R] [One R] [BEq R] [LawfulBEq R] (p : MvPoly n R cmp) :

Nat → MvPoly n R cmp

Exponentiation by repeated squaring.

Equations

p.npowBySq 0 = 1
p.npowBySq k.succ = if (k + 1) % 2 = 0 then p.npowBySq ((k + 1) / 2) * p.npowBySq ((k + 1) / 2) else p.npowBySq ((k + 1) / 2) * p.npowBySq ((k + 1) / 2) * p

Instances For

source

@[instance_reducible]

instance Hex.MvPoly.instPowNatOfAddOfMulOfOneOfLawfulBEq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [Add R] [Mul R] [Zero R] [One R] [BEq R] [LawfulBEq R] :

Pow (MvPoly n R cmp) Nat

Equations

Hex.MvPoly.instPowNatOfAddOfMulOfOneOfLawfulBEq = { pow := Hex.MvPoly.npowBySq }

source

@[simp]

theorem Hex.MvPoly.coeff_one {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (m : Mono n) :

coeff m 1 = if m = Mono.zero then 1 else 0

The coefficient of one is one at the zero monomial and zero elsewhere.

source

theorem Hex.MvPoly.coeff_add {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (m : Mono n) (p q : MvPoly n R cmp) :

coeff m (p + q) = coeff m p + coeff m q

Coefficients distribute over polynomial addition.

source

theorem Hex.MvPoly.add_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) :

p + 0 = p

Zero is a right identity for polynomial addition.

source

theorem Hex.MvPoly.zero_add {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) :

0 + p = p

Zero is a left identity for polynomial addition.

source

theorem Hex.MvPoly.add_comm {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p q : MvPoly n R cmp) :

p + q = q + p

Polynomial addition is commutative.

source

theorem Hex.MvPoly.add_assoc {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p q r : MvPoly n R cmp) :

p + q + r = p + (q + r)

Polynomial addition is associative.

source

theorem Hex.MvPoly.addMonomial_eq {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) (m : Mono n) (c : R) :

p.addMonomial m c = p + monomial m c

Adding a monomial is ordinary addition by a monomial polynomial.

source

theorem Hex.MvPoly.coeff_neg {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Ring R] [DecidableEq R] (m : Mono n) (p : MvPoly n R cmp) :

coeff m (-p) = -coeff m p

Coefficients commute with polynomial negation.

source

theorem Hex.MvPoly.coeff_sub {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Ring R] [DecidableEq R] (m : Mono n) (p q : MvPoly n R cmp) :

coeff m (p - q) = coeff m p - coeff m q

Coefficients distribute over polynomial subtraction.

source

theorem Hex.MvPoly.coeff_mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (m : Mono n) (p q : MvPoly n R cmp) :

coeff m (p * q) = List.foldl (fun (acc : R) (ab : Mono n × Mono n) => acc + coeff ab.fst p * coeff ab.snd q) 0 m.splits

A product coefficient is the convolution over monomial splittings.

source

theorem Hex.MvPoly.mul_zero {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) :

p * 0 = 0

Zero is absorbing on the right for polynomial multiplication.

source

theorem Hex.MvPoly.zero_mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) :

0 * p = 0

Zero is absorbing on the left for polynomial multiplication.

source

theorem Hex.MvPoly.mul_add {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p q r : MvPoly n R cmp) :

p * (q + r) = p * q + p * r

Polynomial multiplication distributes over addition on the right.

source

theorem Hex.MvPoly.add_mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p q r : MvPoly n R cmp) :

(p + q) * r = p * r + q * r

Polynomial multiplication distributes over addition on the left.

source

theorem Hex.MvPoly.monomial_mul_monomial {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (a b : Mono n) (ca cb : R) :

monomial a ca * monomial b cb = monomial (a.mul b) (ca * cb)

Multiplying monomial polynomials multiplies their coefficients and monomials.

source

theorem Hex.MvPoly.powBySq_monomial {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (m : Mono n) (c : R) (k : Nat) :

Mono.powBySq (monomial m c) k = monomial (Mono.scale k m) (Mono.powBySq c k)

Binary powering of a monomial polynomial scales its exponent vector.

source

theorem Hex.MvPoly.mul_one {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) :

p * 1 = p

One is a right identity for polynomial multiplication.

source

theorem Hex.MvPoly.one_mul {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) :

1 * p = p

One is a left identity for polynomial multiplication.

source

theorem Hex.MvPoly.mul_assoc {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p q r : MvPoly n R cmp) :

p * q * r = p * (q * r)

Polynomial multiplication is associative.

source

theorem Hex.MvPoly.mul_comm {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.CommSemiring R] [DecidableEq R] (p q : MvPoly n R cmp) :

p * q = q * p

Polynomial multiplication is commutative over a commutative coefficient semiring.

source

theorem Hex.MvPoly.pow_succ {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) (k : Nat) :

p ^ (k + 1) = p ^ k * p

Polynomial exponentiation satisfies the successor recurrence.

source

theorem Hex.MvPoly.coeff_pow_succ {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (m : Mono n) (p : MvPoly n R cmp) (k : Nat) :

coeff m (p ^ (k + 1)) = coeff m (p ^ k * p)

Coefficients of a successor power are given by multiplication with the preceding power.

source

theorem Hex.MvPoly.npowBySq_eq_pow {n : Nat} {R : Type u} {cmp : Mono n → Mono n → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [Lean.Grind.Semiring R] [DecidableEq R] (p : MvPoly n R cmp) (k : Nat) :

p.npowBySq k = p ^ k

Binary polynomial powering agrees with the public power operation.