Computable monomials

Monomials of the form X₀ᵃ * X₁ᵇ * ... * Xₖᶻ. These are represented as vectors of natural numbers, where each element corresponds to the exponent of a variable.

Main definitions

• CPoly.CMvMonomial n: The type of monomials in n variables, implemented as Vector ℕ n.

def CPoly.CMvMonomial (n : ℕ) : Type

Monomial in n variables.

• #v[e₀, e₁, e₂] denotes X₀^e₀ * X₁^e₁ * X₂^e₂

Equations

• CPoly.CMvMonomial n = Vector ℕ n

def CPoly.«term#m[_]» : Lean.ParserDescr

Equations

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

instance CPoly.instReprCMvMonomial {n : ℕ} : Repr (CMvMonomial n)

Equations

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

instance CPoly.instGetElemCMvMonomialNatLt {n : ℕ} : GetElem (CMvMonomial n) ℕ ℕ fun (x : CMvMonomial n) (idx : ℕ) => idx < n

Equations

• CPoly.instGetElemCMvMonomialNatLt = inferInstanceAs (GetElem (Vector ℕ n) ℕ ℕ fun (x : Vector ℕ n) (i : ℕ) => i < n)

instance CPoly.instGetElem?CMvMonomialNatLt {n : ℕ} : GetElem? (CMvMonomial n) ℕ ℕ fun (x : CMvMonomial n) (idx : ℕ) => idx < n

Equations

• CPoly.instGetElem?CMvMonomialNatLt = inferInstanceAs (GetElem? (Vector ℕ n) ℕ ℕ fun (x : Vector ℕ n) (i : ℕ) => i < n)

instance CPoly.instDecidableEqCMvMonomial {n : ℕ} : DecidableEq (CMvMonomial n)

Equations

• CPoly.instDecidableEqCMvMonomial = inferInstanceAs (DecidableEq (Vector ℕ n))

instance CPoly.instOrdCMvMonomial {n : ℕ} : Ord (CMvMonomial n)

Equations

• CPoly.instOrdCMvMonomial = inferInstanceAs (Ord (Vector ℕ n))

instance CPoly.instTransCmpCMvMonomialCompare {n : ℕ} : Std.TransCmp compare

instance CPoly.instLawfulEqCmpCMvMonomialCompare {n : ℕ} : Std.LawfulEqCmp compare

theorem CPoly.CMvMonomial.ext {n : ℕ} {m₁ m₂ : CMvMonomial n} (h : ∀ (i : ℕ) (x : i < n), m₁[i] = m₂[i]) : m₁ = m₂

theorem CPoly.CMvMonomial.ext_iff {n : ℕ} {m₁ m₂ : CMvMonomial n} : m₁ = m₂ ↔ ∀ (i : ℕ) (x : i < n), m₁[i] = m₂[i]

def CPoly.CMvMonomial.extend {n : ℕ} (n' : ℕ) (m : CMvMonomial n) : CMvMonomial (max n n')

Extend a monomial to a larger number of variables by padding with zeros.

Equations

• CPoly.CMvMonomial.extend n' m = cast ⋯ (Vector.append m (Vector.replicate (n' - n) 0))

def CPoly.CMvMonomial.totalDegree {n : ℕ} (m : CMvMonomial n) : ℕ

The total degree of a monomial (sum of all exponents).

Equations

• m.totalDegree = Vector.sum m

def CPoly.CMvMonomial.degreeOf {n : ℕ} (m : CMvMonomial n) (i : Fin n) : ℕ

The degree of the $i$-th variable in the monomial.

Equations

• m.degreeOf i = Vector.get m i

def CPoly.CMvMonomial.zero {n : ℕ} : CMvMonomial n

The zero monomial (all exponents are zero).

Equations

• CPoly.CMvMonomial.zero = Vector.replicate n 0

instance CPoly.CMvMonomial.instZero {n : ℕ} : Zero (CMvMonomial n)

Equations

• CPoly.CMvMonomial.instZero = { zero := CPoly.CMvMonomial.zero }

def CPoly.CMvMonomial.add {n : ℕ} : CMvMonomial n → CMvMonomial n → CMvMonomial n

Monomial multiplication (adds exponents element-wise).

Equations

• CPoly.CMvMonomial.add = Vector.zipWith Nat.add

instance CPoly.CMvMonomial.instAdd {n : ℕ} : Add (CMvMonomial n)

Equations

• CPoly.CMvMonomial.instAdd = { add := CPoly.CMvMonomial.add }

@[simp]

theorem CPoly.CMvMonomial.add_zero {n : ℕ} {m : CMvMonomial n} : m + 0 = m

def CPoly.CMvMonomial.divides {n : ℕ} (m₁ m₂ : CMvMonomial n) : Bool

Check if $m_1$ divides $m_2$ (true if all exponents of $m_1$ are $\le$ those of $m_2$).

Equations

• m₁.divides m₂ = (Vector.zipWith (flip Nat.ble) m₁ m₂).all fun (x : Bool) => x == true

instance CPoly.CMvMonomial.instDvd {n : ℕ} : Dvd (CMvMonomial n)

Equations

• CPoly.CMvMonomial.instDvd = { dvd := fun (m₁ m₂ : CPoly.CMvMonomial n) => m₁.divides m₂ = true }

instance CPoly.CMvMonomial.instDecidableDvd {n : ℕ} {m₁ m₂ : CMvMonomial n} : Decidable (m₁ ∣ m₂)

Equations

• CPoly.CMvMonomial.instDecidableDvd = id inferInstance

def CPoly.CMvMonomial.div {n : ℕ} (m₁ m₂ : CMvMonomial n) : CMvMonomial n

The monomial division $m_1 / m_2$ (subtracts exponents element-wise).

The result makes sense assuming m₂ | m₁.

Equations

• m₁.div m₂ = Vector.zipWith Nat.sub m₁ m₂

instance CPoly.CMvMonomial.instDiv {n : ℕ} : Div (CMvMonomial n)

Equations

• CPoly.CMvMonomial.instDiv = { div := CPoly.CMvMonomial.div }

instance CPoly.CMvMonomial.instDecidableDvd_1 {n : ℕ} {m₁ m₂ : CMvMonomial n} : Decidable (m₁ ∣ m₂)

Equations

• CPoly.CMvMonomial.instDecidableDvd_1 = id inferInstance

def CPoly.CMvMonomial.toFinsupp {n : ℕ} (m : CMvMonomial n) : Fin n →₀ ℕ

Convert a CMvMonomial to a Finsupp.

Equations

• m.toFinsupp = { support := {i : Fin n | m[i] ≠ 0}, toFun := Vector.get m, mem_support_toFun := ⋯ }

def CPoly.CMvMonomial.ofFinsupp {n : ℕ} (m : Fin n →₀ ℕ) : CMvMonomial n

Convert a Finsupp to a CMvMonomial.

Equations

• CPoly.CMvMonomial.ofFinsupp m = Vector.ofFn ⇑m

@[simp]

theorem CPoly.CMvMonomial.ofFinsupp_toFinsupp {n : ℕ} {m : CMvMonomial n} : ofFinsupp m.toFinsupp = m

@[simp]

theorem CPoly.CMvMonomial.toFinsupp_ofFinsupp {n : ℕ} {m : Fin n →₀ ℕ} : (ofFinsupp m).toFinsupp = m

theorem CPoly.CMvMonomial.injective_ofFinsupp {n : ℕ} : Function.Injective ofFinsupp

theorem CPoly.CMvMonomial.injective_toFinsupp {n : ℕ} : Function.Injective toFinsupp

def CPoly.CMvMonomial.equivFinsupp {n : ℕ} : CMvMonomial n ≃ (Fin n →₀ ℕ)

Equations

• CPoly.CMvMonomial.equivFinsupp = { toFun := CPoly.CMvMonomial.toFinsupp, invFun := CPoly.CMvMonomial.ofFinsupp, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CPoly.CMvMonomial.map_mul {n : ℕ} {m₁ m₂ : Multiplicative (Fin n →₀ ℕ)} : ofFinsupp (m₁ * m₂) = ofFinsupp m₁ + ofFinsupp m₂

@[reducible, inline]

abbrev CPoly.MonoR (n : ℕ) (R : Type) : Type

Equations

• CPoly.MonoR n R = (CPoly.CMvMonomial n × R)

instance CPoly.MonoR.instDecidableEqProdCMvMonomial {n : ℕ} {R : Type} [DecidableEq R] : DecidableEq (CMvMonomial n × R)

Equations

• CPoly.MonoR.instDecidableEqProdCMvMonomial = instDecidableEqProd

instance CPoly.MonoR.instRepr {n : ℕ} {R : Type} [Repr R] : Repr (MonoR n R)

Equations

• CPoly.MonoR.instRepr = { reprPrec := fun (x : CPoly.MonoR n R) (x_1 : ℕ) => match x, x_1 with | (m, c), x => repr c ++ Std.Format.text " * " ++ repr m }

def CPoly.MonoR.C {n : ℕ} {R : Type} (c : R) : MonoR n R

Equations

• CPoly.MonoR.C c = (CPoly.CMvMonomial.zero, c)

def CPoly.MonoR.divides {n : ℕ} {R : Type} [CommSemiring R] [HMod R R R] [BEq R] (t₁ t₂ : MonoR n R) : Bool

Equations

• t₁.divides t₂ = decide (t₁.1 ∣ t₂.1 ∧ (t₁.2 % t₂.2 == 0) = true)

instance CPoly.MonoR.instDvd {n : ℕ} {R : Type} [CommSemiring R] [HMod R R R] [BEq R] : Dvd (MonoR n R)

Equations

• CPoly.MonoR.instDvd = { dvd := fun (t₁ t₂ : CPoly.MonoR n R) => t₁.divides t₂ = true }

instance CPoly.MonoR.instDecidableDvd {n : ℕ} {R : Type} [CommSemiring R] [HMod R R R] [BEq R] {t₁ t₂ : MonoR n R} : Decidable (t₁ ∣ t₂)

Equations

• CPoly.MonoR.instDecidableDvd = id inferInstance

def CPoly.MonoR.evalMonomial {R : Type} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvMonomial n → R

Equations

• CPoly.MonoR.evalMonomial vals m = ∏ i : Fin n, vals i ^ Vector.get m i

@[reducible]

def Finsupp.ofCMvMonomial {n : ℕ} (m : CPoly.CMvMonomial n) : Fin n →₀ ℕ

Alias of CPoly.CMvMonomial.toFinsupp.

---

Convert a CMvMonomial to a Finsupp.

Equations

• @Finsupp.ofCMvMonomial = @CPoly.CMvMonomial.toFinsupp

@[reducible]

def Finsupp.toCMvMonomial {n : ℕ} (m : Fin n →₀ ℕ) : CPoly.CMvMonomial n

Alias of CPoly.CMvMonomial.ofFinsupp.

---

Convert a Finsupp to a CMvMonomial.

Equations

• @Finsupp.toCMvMonomial = @CPoly.CMvMonomial.ofFinsupp