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.

@[implicit_reducible]

def CPoly.CMvMonomial (n : ℕ) : Type

Monomial in n variables.

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

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

instance CPoly.instOrdCMvMonomial {n : ℕ} : Ord (CMvMonomial 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.

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

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

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

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

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

The zero monomial (all exponents are zero).

@[instance_reducible]

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

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

Monomial multiplication (adds exponents element-wise).

@[instance_reducible]

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

@[simp]

theorem CPoly.CMvMonomial.getElem_add {n : ℕ} {m₁ m₂ : CMvMonomial n} (i : ℕ) (h : i < n) : (m₁ + m₂)[i] = m₁[i] + m₂[i]

@[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$).

@[instance_reducible]

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

@[instance_reducible]

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

theorem CPoly.CMvMonomial.dvd_iff_divides {n : ℕ} {m₁ m₂ : CMvMonomial n} : m₁ ∣ m₂ ↔ m₁.divides m₂ = true

theorem CPoly.CMvMonomial.dvd_iff {n : ℕ} {m₁ m₂ : CMvMonomial n} : m₁ ∣ m₂ ↔ ∀ (i : ℕ) (h : i < n), m₁[i] ≤ m₂[i]

m₁ ∣ m₂ holds exactly when every exponent of m₁ is at most the matching exponent of m₂.

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₁.

@[instance_reducible]

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

@[simp]

theorem CPoly.CMvMonomial.getElem_div {n : ℕ} {m₁ m₂ : CMvMonomial n} (i : ℕ) (h : i < n) : (m₁ / m₂)[i] = m₁[i] - m₂[i]

theorem CPoly.CMvMonomial.add_div_of_dvd {n : ℕ} {m₁ m₂ : CMvMonomial n} (h : m₁ ∣ m₂) : m₁ + m₂ / m₁ = m₂

theorem CPoly.CMvMonomial.dvd_iff_exists_add {n : ℕ} {m₁ m₂ : CMvMonomial n} : m₁ ∣ m₂ ↔ ∃ (c : CMvMonomial n), m₂ = m₁ + c

Divisibility agrees with monomial multiplication, which adds exponents.

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

Convert a CMvMonomial to a Finsupp.

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

Convert a Finsupp to a CMvMonomial.

@[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.dvd_iff_toFinsupp_le {n : ℕ} {m₁ m₂ : CMvMonomial n} : m₁ ∣ m₂ ↔ m₁.toFinsupp ≤ m₂.toFinsupp

Divisibility is the pointwise order on exponent vectors.

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 →₀ ℕ)

@[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 u_1) : Type u_1

@[instance_reducible]

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

@[instance_reducible]

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

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

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

Check if $t_1$ divides $t_2$: the monomial of $t_1$ divides that of $t_2$, and the coefficient of $t_2$ is zero modulo that of $t_1$.

@[instance_reducible]

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

@[instance_reducible]

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

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

@[reducible]

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

Alias of CPoly.CMvMonomial.toFinsupp.

---

Convert a CMvMonomial to a Finsupp.

@[reducible]

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

Alias of CPoly.CMvMonomial.ofFinsupp.

---

Convert a Finsupp to a CMvMonomial.