@[reducible, inline]

abbrev Hex.Mono (n : Nat) : Type

An exponent vector for n ordered variables.

Equations

• Hex.Mono n = Vector Nat n

def Hex.Mono.zero {n : Nat} : Mono n

The constant monomial.

Equations

• Hex.Mono.zero = Hex.Vector.ofFn' fun (x : Fin n) => 0

@[instance_reducible]

instance Hex.Mono.instInhabited {n : Nat} : Inhabited (Mono n)

Equations

• Hex.Mono.instInhabited = { default := Hex.Mono.zero }

def Hex.Mono.unit {n : Nat} (i : Fin n) : Mono n

The monomial consisting of one copy of variable i.

Equations

• Hex.Mono.unit i = Hex.Vector.ofFn' fun (j : Fin n) => if j = i then 1 else 0

def Hex.Mono.mul {n : Nat} (a b : Mono n) : Mono n

Monomial multiplication, represented by pointwise exponent addition.

Equations

• a.mul b = Hex.Vector.ofFn' fun (i : Fin n) => a[i] + b[i]

def Hex.Mono.scale {n : Nat} (k : Nat) (m : Mono n) : Mono n

Multiply every exponent by k.

Equations

• Hex.Mono.scale k m = Hex.Vector.ofFn' fun (i : Fin n) => k * m[i]

def Hex.Mono.dvd {n : Nat} (a b : Mono n) : Bool

Whether a divides b, i.e. whether every exponent of a is at most the corresponding exponent of b.

Equations

• a.dvd b = decide (∀ (i : Fin n), a[i] ≤ b[i])

def Hex.Mono.div {n : Nat} (a b : Mono n) : Option (Mono n)

The exact quotient b / a, returning none when a does not divide b.

Equations

• a.div b = if h : ∀ (i : Fin n), a[i] ≤ b[i] then some (Hex.Vector.ofFn' fun (i : Fin n) => b[i] - a[i]) else none

def Hex.Mono.lcm {n : Nat} (a b : Mono n) : Mono n

Pointwise maximum of two monomials.

Equations

• a.lcm b = Hex.Vector.ofFn' fun (i : Fin n) => max a[i] b[i]

def Hex.Mono.gcd {n : Nat} (a b : Mono n) : Mono n

Pointwise minimum of two monomials.

Equations

• a.gcd b = Hex.Vector.ofFn' fun (i : Fin n) => min a[i] b[i]

def Hex.Mono.degree {n : Nat} (m : Mono n) : Nat

Total degree of a monomial.

Equations

• m.degree = List.foldl (fun (acc : Nat) (i : Fin n) => acc + m[i]) 0 (List.finRange n)

def Hex.Mono.degreeOf {n : Nat} (i : Fin n) (m : Mono n) : Nat

Exponent of variable i in a monomial.

Equations

• Hex.Mono.degreeOf i m = m[i]

def Hex.Mono.support {n : Nat} (m : Mono n) : List (Fin n)

Variables occurring with positive exponent, in increasing index order.

Equations

• m.support = List.filter (fun (i : Fin n) => m[i] != 0) (List.finRange n)

def Hex.Mono.rename {n k : Nat} (f : Fin n → Fin k) (m : Mono n) : Mono k

Rename variables, adding exponents when several source variables map to the same target variable.

Equations

• Hex.Mono.rename f m = Hex.Vector.ofFn' fun (j : Fin k) => List.foldl (fun (acc : Nat) (i : Fin n) => acc + if f i = j then m[i] else 0) 0 (List.finRange n)

def Hex.Mono.succAt {n : Nat} (i : Fin n) (m : Mono n) : Mono n

Increase the exponent of variable i by one.

Equations

• Hex.Mono.succAt i m = m.mul (Hex.Mono.unit i)

def Hex.Mono.dropHead {n : Nat} (m : Mono (n + 1)) : Mono n

Remove the first exponent from a nonempty monomial.

Equations

• m.dropHead = Hex.Vector.ofFn' fun (i : Fin n) => m[i.succ]

def Hex.Mono.prepend {n : Nat} (e : Nat) (m : Mono n) : Mono (n + 1)

Add an exponent at the front of a monomial.

Equations

• Hex.Mono.prepend e m = Hex.Vector.ofFn' fun (i : Fin (n + 1)) => if h : ↑i = 0 then e else m[↑i - 1]

def Hex.Mono.splits {n : Nat} : Mono n → List (Mono n × Mono n)

All decompositions a * b = m. Each exponent is split independently, so the list has ∏ i, (m[i] + 1) entries.

Equations

• One or more equations did not get rendered due to their size.
• x_2.splits = [(Hex.Mono.zero, Hex.Mono.zero)]

@[irreducible]

def Hex.Mono.powBySq {R : Type u_1} [One R] [Mul R] (a : R) : Nat → R

Exponentiation by repeated squaring, used here so monomial evaluation does not depend on a coefficient type's choice of Pow implementation.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Mono.powBySq a 0 = 1

theorem Hex.Mono.powBySq_eq_pow {R : Type u_1} [Lean.Grind.Semiring R] (a : R) (k : Nat) : powBySq a k = a ^ k

Repeated-squaring exponentiation agrees with the semiring power.

def Hex.Mono.prod {R : Type u_1} {n : Nat} [One R] [Mul R] (x : Fin n → R) (m : Mono n) : R

Evaluate a monomial at x, using logarithmic exponentiation for each variable.

Equations

• Hex.Mono.prod x m = List.foldl (fun (acc : R) (i : Fin n) => acc * Hex.Mono.powBySq (x i) m[i]) 1 (List.finRange n)

def Hex.Mono.lex {n : Nat} (a b : Mono n) : Ordering

Plain lexicographic comparison, with the first variable most significant.

Equations

• a.lex b = List.compareLex compare (Vector.toList a) (Vector.toList b)

def Hex.Mono.grlex {n : Nat} (a b : Mono n) : Ordering

Graded lexicographic comparison: total degree first, then lex.

Equations

• a.grlex b = compareLex (fun (x y : Hex.Mono n) => compare x.degree y.degree) Hex.Mono.lex a b

def Hex.Mono.revlex {n : Nat} (a b : Mono n) : Ordering

Reverse-lexicographic tie breaker used by grevlex.

Equations

• a.revlex b = List.compareLex (fun (x y : Nat) => compare y x) (Vector.toList a).reverse (Vector.toList b).reverse

def Hex.Mono.grevlex {n : Nat} (a b : Mono n) : Ordering

Graded reverse lexicographic comparison: total degree first; among equal-degree monomials, the monomial with the larger exponent in the last differing variable compares smaller.

Equations

• a.grevlex b = compareLex (fun (x y : Hex.Mono n) => compare x.degree y.degree) Hex.Mono.revlex a b

instance Hex.Mono.instLexTransCmp {n : Nat} : Std.TransCmp lex

instance Hex.Mono.instLexLawfulEqCmp {n : Nat} : Std.LawfulEqCmp lex

instance Hex.Mono.instRevlexTransCmp {n : Nat} : Std.TransCmp revlex

instance Hex.Mono.instRevlexLawfulEqCmp {n : Nat} : Std.LawfulEqCmp revlex

instance Hex.Mono.instGrlexTransCmp {n : Nat} : Std.TransCmp grlex

instance Hex.Mono.instGrlexLawfulEqCmp {n : Nat} : Std.LawfulEqCmp grlex

instance Hex.Mono.instGrevlexTransCmp {n : Nat} : Std.TransCmp grevlex

instance Hex.Mono.instGrevlexLawfulEqCmp {n : Nat} : Std.LawfulEqCmp grevlex

class Hex.IsMonomialOrder {n : Nat} (cmp : Mono n → Mono n → Ordering) extends Std.TransCmp cmp, Std.LawfulEqCmp cmp : Prop

Laws needed of a comparator by leading-term and reduction algorithms. Storage itself uses the inherited TransCmp and LawfulEqCmp laws.

• eq_swap {a b : Hex.Mono n} : cmp a b = (cmp b a).swap
• isLE_trans {a b c : Hex.Mono n} : (cmp a b).isLE = true → (cmp b c).isLE = true → (cmp a c).isLE = true
• compare_self {a : Hex.Mono n} : cmp a a = Ordering.eq
• eq_of_compare {a b : Hex.Mono n} : cmp a b = Ordering.eq → a = b
• zero_le (m : Mono n) : cmp Mono.zero m ≠ Ordering.gt

  The constant monomial is least.

• mul_mono (a b c : Mono n) : cmp a b = cmp (a.mul c) (b.mul c)

  Multiplying both sides by the same monomial preserves comparison.

• wf : WellFounded fun (a b : Mono n) => cmp a b = Ordering.lt

  Strict comparison is well founded.

@[simp]

theorem Hex.Mono.getElem_zero {n : Nat} (i : Fin n) : zero[i] = 0

Every exponent of the zero monomial is zero.

@[simp]

theorem Hex.Mono.getElem_unit {n : Nat} (i j : Fin n) : (unit i)[j] = if j = i then 1 else 0

A unit monomial has exponent one at its selected variable and zero elsewhere.

@[simp]

theorem Hex.Mono.getElem_mul {n : Nat} (a b : Mono n) (i : Fin n) : (a.mul b)[i] = a[i] + b[i]

Monomial multiplication adds exponents pointwise.

@[simp]

theorem Hex.Mono.zero_mul {n : Nat} (m : Mono n) : zero.mul m = m

The zero monomial is a left identity for monomial multiplication.

@[simp]

theorem Hex.Mono.mul_zero {n : Nat} (m : Mono n) : m.mul zero = m

The zero monomial is a right identity for monomial multiplication.

theorem Hex.Mono.mul_assoc {n : Nat} (a b c : Mono n) : (a.mul b).mul c = a.mul (b.mul c)

Monomial multiplication is associative.

theorem Hex.Mono.mul_comm {n : Nat} (a b : Mono n) : a.mul b = b.mul a

Monomial multiplication is commutative.

@[simp]

theorem Hex.Mono.getElem_scale {n : Nat} (k : Nat) (m : Mono n) (i : Fin n) : (scale k m)[i] = k * m[i]

Scaling a monomial multiplies every exponent by the scale.

@[simp]

theorem Hex.Mono.zero_scale {n : Nat} (m : Mono n) : scale 0 m = zero

Scaling by zero yields the zero monomial.

@[simp]

theorem Hex.Mono.scale_zero {n : Nat} (k : Nat) : scale k zero = zero

Every scaling of the zero monomial is zero.

@[simp]

theorem Hex.Mono.one_scale {n : Nat} (m : Mono n) : scale 1 m = m

Scaling by one leaves a monomial unchanged.

theorem Hex.Mono.add_scale {n : Nat} (a b : Nat) (m : Mono n) : scale (a + b) m = (scale a m).mul (scale b m)

Scaling by a sum is multiplication of the separately scaled monomials.

theorem Hex.Mono.mul_units {n : Nat} (m : Mono n) : List.foldl (fun (acc : Mono n) (i : Fin n) => acc.mul (scale m[i] (unit i))) zero (List.finRange n) = m

Every monomial is the product of its scaled unit monomials.

@[simp]

theorem Hex.Mono.getElem_lcm {n : Nat} (a b : Mono n) (i : Fin n) : (a.lcm b)[i] = max a[i] b[i]

The monomial least common multiple takes pointwise maximum exponents.

@[simp]

theorem Hex.Mono.getElem_gcd {n : Nat} (a b : Mono n) (i : Fin n) : (a.gcd b)[i] = min a[i] b[i]

The monomial greatest common divisor takes pointwise minimum exponents.

@[simp]

theorem Hex.Mono.getElem_dropHead {n : Nat} (m : Mono (n + 1)) (i : Fin n) : m.dropHead[i] = m[i.succ]

Dropping the head shifts every remaining exponent down one coordinate.

@[simp]

theorem Hex.Mono.getElem_prepend_zero {n : Nat} (e : Nat) (m : Mono n) : (prepend e m)[0] = e

The head of a prepended monomial is the supplied exponent.

@[simp]

theorem Hex.Mono.getElem_prepend_succ {n : Nat} (e : Nat) (m : Mono n) (i : Fin n) : (prepend e m)[i.succ] = m[i]

The tail of a prepended monomial contains the original exponents.

@[simp]

theorem Hex.Mono.dropHead_prepend {n : Nat} (e : Nat) (m : Mono n) : (prepend e m).dropHead = m

Dropping a freshly prepended exponent recovers the original monomial.

theorem Hex.Mono.prepend_head_dropHead {n : Nat} (m : Mono (n + 1)) : prepend (Vector.head m) m.dropHead = m

Prepending a monomial's head to its tail reconstructs it.

theorem Hex.Mono.mul_prepend {n : Nat} (ea eb : Nat) (a b : Mono n) : (prepend ea a).mul (prepend eb b) = prepend (ea + eb) (a.mul b)

Multiplication distributes across prepended exponent vectors.

theorem Hex.Mono.dropHead_mul {n : Nat} (a b : Mono (n + 1)) : (a.mul b).dropHead = a.dropHead.mul b.dropHead

Dropping the head commutes with monomial multiplication.

theorem Hex.Mono.dvd_eq_true_iff {n : Nat} (a b : Mono n) : a.dvd b = true ↔ ∀ (i : Fin n), a[i] ≤ b[i]

Boolean monomial divisibility is pointwise exponent comparison.

theorem Hex.Mono.div_eq_some_iff {n : Nat} (a b q : Mono n) : a.div b = some q ↔ a.mul q = b

Exact monomial division returns a quotient exactly when multiplying it back recovers the dividend.

theorem Hex.Mono.div_eq_none_iff {n : Nat} (a b : Mono n) : a.div b = none ↔ ¬∀ (i : Fin n), a[i] ≤ b[i]

Exact monomial division fails exactly when the divisor does not divide.

theorem Hex.Mono.degree_mul {n : Nat} (a b : Mono n) : (a.mul b).degree = a.degree + b.degree

Total degree is additive under monomial multiplication.

@[simp]

theorem Hex.Mono.toList_prepend {n : Nat} (e : Nat) (m : Mono n) : Vector.toList (prepend e m) = e :: Vector.toList m

Converting a prepended monomial to a list prepends the exponent.

theorem Hex.Mono.toList_mul {n : Nat} (a b : Mono n) : Vector.toList (a.mul b) = List.zipWith (fun (x1 x2 : Nat) => x1 + x2) (Vector.toList a) (Vector.toList b)

The exponent list of a product is the pointwise sum of exponent lists.

theorem Hex.Mono.lex_prepend {n : Nat} (ea eb : Nat) (a b : Mono n) : (prepend ea a).lex (prepend eb b) = (compare ea eb).then (a.lex b)

Lexicographic comparison of prepended monomials first compares their heads.

instance Hex.Mono.instLexOrder {n : Nat} : IsMonomialOrder lex

@[simp]

theorem Hex.Mono.degree_zero {n : Nat} : zero.degree = 0

The zero monomial has total degree zero.

instance Hex.Mono.instGrlexOrder {n : Nat} : IsMonomialOrder grlex

theorem Hex.Mono.degreeOf_le_degree {n : Nat} (i : Fin n) (m : Mono n) : degreeOf i m ≤ m.degree

Every individual exponent is bounded by total degree.

instance Hex.Mono.instGrevlexOrder {n : Nat} : IsMonomialOrder grevlex

theorem Hex.Mono.rename_mul {n k : Nat} (f : Fin n → Fin k) (a b : Mono n) : rename f (a.mul b) = (rename f a).mul (rename f b)

Renaming variables commutes with monomial multiplication.

theorem Hex.Mono.splits_mem_iff {n : Nat} (m a b : Mono n) : (a, b) ∈ m.splits ↔ a.mul b = m

A pair occurs in splits m exactly when its monomial product is m.

theorem Hex.Mono.splits_nodup {n : Nat} (m : Mono n) : m.splits.Nodup

Every monomial decomposition occurs exactly once in splits.

theorem Hex.Mono.dvd_lcm_left {n : Nat} (a b : Mono n) : a.dvd (a.lcm b) = true

The left input divides the monomial least common multiple.

theorem Hex.Mono.dvd_lcm_right {n : Nat} (a b : Mono n) : b.dvd (a.lcm b) = true

The right input divides the monomial least common multiple.

theorem Hex.Mono.lcm_dvd {n : Nat} (a b c : Mono n) (ha : a.dvd c = true) (hb : b.dvd c = true) : (a.lcm b).dvd c = true

The monomial least common multiple divides every common multiple.

theorem Hex.Mono.gcd_dvd_left {n : Nat} (a b : Mono n) : (a.gcd b).dvd a = true

The monomial greatest common divisor divides the left input.

theorem Hex.Mono.gcd_dvd_right {n : Nat} (a b : Mono n) : (a.gcd b).dvd b = true

The monomial greatest common divisor divides the right input.

theorem Hex.Mono.dvd_gcd {n : Nat} (a b c : Mono n) (ha : c.dvd a = true) (hb : c.dvd b = true) : c.dvd (a.gcd b) = true

Every common divisor divides the monomial greatest common divisor.