Unlawful multivariate polynomials

This file defines the Unlawful type, which represents multivariate polynomials as a map from monomials to coefficients. Unlike Lawful, it does not enforce the absence of zero coefficients.

Main definitions

• CPoly.Unlawful n R: A map from CMvMonomial n to R, implemented using Std.ExtTreeMap.

@[reducible, inline]

abbrev CPoly.Unlawful (n : ℕ) (R : Type u_1) : Type u_1

Polynomial in n variables with coefficients in R. Internally represented as a tree map from monomials to coefficients.

@[instance_reducible]

instance CPoly.instEmptyCollectionUnlawful {n : ℕ} {R : Type u_1} : EmptyCollection (Unlawful n R)

@[instance_reducible]

instance CPoly.instSingletonMonoRUnlawful {n : ℕ} {R : Type u_1} : Singleton (MonoR n R) (Unlawful n R)

@[instance_reducible]

instance CPoly.instInsertMonoRUnlawful {n : ℕ} {R : Type u_1} : Insert (MonoR n R) (Unlawful n R)

instance CPoly.instLawfulSingletonMonoRUnlawful {n : ℕ} {R : Type u_1} : LawfulSingleton (MonoR n R) (Unlawful n R)

@[instance_reducible]

instance CPoly.instMembershipCMvMonomialUnlawful {n : ℕ} {R : Type u_1} : Membership (CMvMonomial n) (Unlawful n R)

@[instance_reducible, instance 10000, defaultInstance 1000]

instance CPoly.instGetElemUnlawfulCMvMonomialMem {n : ℕ} {R : Type u_1} : GetElem (Unlawful n R) (CMvMonomial n) R fun (lp : Unlawful n R) (m : CMvMonomial n) => m ∈ lp

@[instance_reducible]

instance CPoly.instGetElem?UnlawfulCMvMonomialMem {n : ℕ} {R : Type u_1} : GetElem? (Unlawful n R) (CMvMonomial n) R fun (lp : Unlawful n R) (m : CMvMonomial n) => m ∈ lp

instance CPoly.instLawfulGetElemUnlawfulCMvMonomialMem {n : ℕ} {R : Type u_1} : LawfulGetElem (Unlawful n R) (CMvMonomial n) R fun (lp : Unlawful n R) (m : CMvMonomial n) => m ∈ lp

theorem CPoly.Unlawful.ext_getElem? {n : ℕ} {R : Type u_1} {t₁ t₂ : Unlawful n R} (h : ∀ (k : CMvMonomial n), t₁[k]? = t₂[k]?) : t₁ = t₂

theorem CPoly.Unlawful.ext_getElem?_iff {n : ℕ} {R : Type u_1} {t₁ t₂ : Unlawful n R} : t₁ = t₂ ↔ ∀ (k : CMvMonomial n), t₁[k]? = t₂[k]?

def CPoly.Unlawful.ofList {n : ℕ} {R : Type u_1} (l : List (CMvMonomial n × R)) : Unlawful n R

Construct an Unlawful polynomial from a list of monomial-coefficient pairs.

def CPoly.Unlawful.extend {n : ℕ} {R : Type u_1} (n' : ℕ) (p : Unlawful n R) : Unlawful (max n n') R

Extend the number of variables by padding monomials with zeros.

@[reducible, inline]

abbrev CPoly.Unlawful.isNoZeroCoef {n : ℕ} {R : Type u_1} [Zero R] (p : Unlawful n R) : Prop

Check if the polynomial has no zero coefficients.

def CPoly.Unlawful.toFinset {n : ℕ} {R : Type u_1} [DecidableEq R] (p : Unlawful n R) : Finset (CMvMonomial n × R)

@[reducible, inline]

abbrev CPoly.Unlawful.monomials {n : ℕ} {R : Type u_1} (p : Unlawful n R) : List (CMvMonomial n)

The list of monomials present in the polynomial.

@[simp]

theorem CPoly.Unlawful.mem_monomials {n : ℕ} {R : Type u_1} {m : CMvMonomial n} {up : Unlawful n R} : m ∈ up.monomials ↔ m ∈ up

@[instance_reducible]

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

def CPoly.Unlawful.C {n : ℕ} {R : Type u_1} [BEq R] [LawfulBEq R] [Zero R] (c : R) : Unlawful n R

Constant polynomial.

@[instance_reducible]

instance CPoly.Unlawful.instOfNatOfNatNat {n : ℕ} {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] : OfNat (Unlawful n R) 0

@[instance_reducible]

instance CPoly.Unlawful.instOfNatOfNatCastOfNeZeroNat {n : ℕ} {R : Type u_1} {m : ℕ} [Zero R] [BEq R] [LawfulBEq R] [NatCast R] [NeZero m] : OfNat (Unlawful n R) m

@[simp]

theorem CPoly.Unlawful.C_zero {n : ℕ} {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] : C 0 = 0

@[simp]

theorem CPoly.Unlawful.C_zero' {n : ℕ} : C 0 = 0

@[simp]

theorem CPoly.Unlawful.zero_eq_zero {R : Type u_1} [Zero R] : Zero.zero = 0

theorem CPoly.Unlawful.zero_eq_empty {n : ℕ} {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] : 0 = ∅

@[simp]

theorem CPoly.Unlawful.not_mem_C_zero {n : ℕ} {x : CMvMonomial n} : x ∉ C 0

@[simp]

theorem CPoly.Unlawful.not_mem_zero {n : ℕ} {R : Type u_1} [Zero R] {x : CMvMonomial n} [BEq R] [LawfulBEq R] : x ∉ 0

@[simp]

theorem CPoly.Unlawful.isNoZeroCoef_zero {n : ℕ} {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] : isNoZeroCoef 0

def CPoly.Unlawful.add {n : ℕ} {R : Type u_1} [Add R] (p₁ p₂ : Unlawful n R) : Unlawful n R

Pointwise addition of coefficients.

@[instance_reducible]

instance CPoly.Unlawful.instAdd {n : ℕ} {R : Type u_1} [Add R] : Add (Unlawful n R)

theorem CPoly.Unlawful.grind_add_skip {n : ℕ} {R : Type u_1} [Add R] {p₁ p₂ : Unlawful n R} : p₁ + p₂ = Std.ExtTreeMap.mergeWith (fun (x : CMvMonomial n) (c₁ c₂ : R) => c₁ + c₂) p₁ p₂

def CPoly.Unlawful.addMonoR {n : ℕ} {R : Type u_1} [Add R] (p : Unlawful n R) (term : MonoR n R) : Unlawful n R

Add a single monomial-coefficient term to a polynomial.

def CPoly.Unlawful.mul₀ {n : ℕ} {R : Type u_1} [Mul R] (t : MonoR n R) (p : Unlawful n R) : Unlawful n R

Multiply a polynomial by a single monomial term.

@[simp]

theorem CPoly.Unlawful.mul₀_zero {n : ℕ} {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] [Mul R] {t : MonoR n R} : mul₀ t 0 = 0

def CPoly.Unlawful.mul {n : ℕ} {R : Type u_1} [Mul R] [Add R] [Zero R] [BEq R] [LawfulBEq R] (p₁ p₂ : Unlawful n R) : Unlawful n R

Polynomial multiplication using a nested fold (distributive law).

@[instance_reducible]

instance CPoly.Unlawful.instMulOfLawfulBEqOfAddOfZero {n : ℕ} {R : Type u_1} [BEq R] [LawfulBEq R] [Mul R] [Add R] [Zero R] : Mul (Unlawful n R)

def CPoly.Unlawful.neg {n : ℕ} {R : Type u_1} [Neg R] (p : Unlawful n R) : Unlawful n R

Negation (negates all coefficients).

@[instance_reducible]

instance CPoly.Unlawful.instNeg {n : ℕ} {R : Type u_1} [Neg R] : Neg (Unlawful n R)

def CPoly.Unlawful.sub {n : ℕ} {R : Type u_1} [Neg R] [Add R] (p₁ p₂ : Unlawful n R) : Unlawful n R

Subtraction.

@[instance_reducible]

instance CPoly.Unlawful.instSubOfAdd {n : ℕ} {R : Type u_1} [Neg R] [Add R] : Sub (Unlawful n R)

def CPoly.Unlawful.leadingTerm? {n : ℕ} {R : Type u_1} : Unlawful n R → Option (MonoR n R)

Return the term with the lexicographically largest monomial.

def CPoly.Unlawful.leadingMonomial? {n : ℕ} {R : Type u_1} : Unlawful n R → Option (CMvMonomial n)

Return the lexicographically largest monomial.

@[instance_reducible]

instance CPoly.Unlawful.instDecidableEq {n : ℕ} {R : Type u_1} [DecidableEq R] : DecidableEq (Unlawful n R)

def CPoly.Unlawful.coeff {R : Type u_2} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : Unlawful n R) : R

@[simp]

theorem CPoly.Unlawful.filter_get {n : ℕ} {R : Type u_2} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial n} (a : Unlawful n R) : (Std.ExtTreeMap.filter (fun (x : CMvMonomial n) (c : R) => c != v) a)[m]?.getD v = a[m]?.getD v

theorem CPoly.Unlawful.add_getD? {n : ℕ} {R : Type u_1} [AddZeroClass R] {m : CMvMonomial n} {p q : Unlawful n R} : (p.add q)[m]?.getD 0 = p[m]?.getD 0 + q[m]?.getD 0