Computable multivariate polynomials (extended operations)

Operations on CMvPolynomial that depend on ring instances from MvPolyEquiv.lean, such as monomial orders, leading terms, restriction, variable renaming, and substitution.

The core type and basic operations (CMvPolynomial, C, X, coeff, eval, etc.) are in CMvPolynomial.lean. The CommSemiring and CommRing instances are in MvPolyEquiv.lean.

Main definitions

• MonomialOrder: Typeclass for comparing monomials.
• leadingMonomial, leadingCoeff, leadingTerm: Leading term operations according to a monomial order.
• rename: Rename variables using a function Fin n → Fin m.
• aeval: Algebra evaluation.
• bind₁: Substitution of polynomials for variables.

Leading-term operations

class CPoly.CMvPolynomial.MonomialOrder (n : ℕ) : Type

Monomial ordering typeclass for n variables.

Provides a way to compare monomials for determining leading terms.

• compare : CMvMonomial n → CMvMonomial n → Ordering

def CPoly.CMvPolynomial.MonomialOrder.degree {n : ℕ} (m : CMvMonomial n) : ℕ

Baseline degree of a monomial.

Currently this is the ordinary total degree and is independent of MonomialOrder.compare.

def CPoly.CMvPolynomial.leadingMonomial {n : ℕ} {R : Type u_2} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : Option (CMvMonomial n)

Leading monomial of a polynomial according to a monomial order.

Returns none for the zero polynomial.

def CPoly.CMvPolynomial.leadingTerm {n : ℕ} {R : Type u_2} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] (p : CMvPolynomial n R) : CMvPolynomial n R

Leading term of a polynomial according to a monomial order.

Returns 0 for the zero polynomial, and otherwise returns the monomial with leading monomial and leading coefficient.

def CPoly.CMvPolynomial.leadingCoeff {n : ℕ} {R : Type u_2} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : R

Leading coefficient of a polynomial according to a monomial order.

Returns 0 for the zero polynomial.

@[simp]

theorem CPoly.CMvPolynomial.leadingCoeff_eq_zero_of_leadingMonomial_eq_none {n : ℕ} {R : Type u_2} [Zero R] [MonomialOrder n] {p : CMvPolynomial n R} (h : p.leadingMonomial = none) : p.leadingCoeff = 0

theorem CPoly.CMvPolynomial.leadingCoeff_eq_coeff_of_leadingMonomial_eq_some {n : ℕ} {R : Type u_2} [Zero R] [MonomialOrder n] {p : CMvPolynomial n R} {m : CMvMonomial n} (h : p.leadingMonomial = some m) : p.leadingCoeff = coeff m p

theorem CPoly.CMvPolynomial.leadingCoeff_eq_coeff_leadingMonomial {n : ℕ} {R : Type u_2} [Zero R] [MonomialOrder n] (p : CMvPolynomial n R) : p.leadingCoeff = p.leadingMonomial.elim 0 fun (m : CMvMonomial n) => coeff m p

Packaged form of leadingCoeff: it is the coefficient at the optional leading monomial, defaulting to 0 when no leading monomial exists.

@[simp]

theorem CPoly.CMvPolynomial.leadingTerm_eq_zero_of_leadingMonomial_eq_none {n : ℕ} {R : Type u_2} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] {p : CMvPolynomial n R} (h : p.leadingMonomial = none) : p.leadingTerm = 0

@[simp]

theorem CPoly.CMvPolynomial.leadingTerm_eq_monomial_of_leadingMonomial_eq_some {n : ℕ} {R : Type u_2} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] {p : CMvPolynomial n R} {m : CMvMonomial n} (h : p.leadingMonomial = some m) : p.leadingTerm = monomial m (coeff m p)

Evaluation and substitution

def CPoly.CMvPolynomial.aeval {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p : CMvPolynomial n R) : σ

Algebra evaluation: evaluates polynomial in an algebra.

Given an algebra σ over R and a function f : Fin n → σ, evaluates the polynomial.

@[simp]

theorem CPoly.CMvPolynomial.aeval_eq_eval₂ {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p : CMvPolynomial n R) : aeval f p = eval₂ (algebraMap R σ) f p

@[simp]

theorem CPoly.CMvPolynomial.aeval_C {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (c : R) : aeval f (C c) = (algebraMap R σ) c

@[simp]

theorem CPoly.CMvPolynomial.aeval_add {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p q : CMvPolynomial n R) : aeval f (p + q) = aeval f p + aeval f q

@[simp]

theorem CPoly.CMvPolynomial.aeval_mul {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p q : CMvPolynomial n R) : aeval f (p * q) = aeval f p * aeval f q

@[simp]

theorem CPoly.CMvPolynomial.aeval_zero {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) : aeval f 0 = 0

@[simp]

theorem CPoly.CMvPolynomial.aeval_one {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) : aeval f 1 = 1

@[simp]

theorem CPoly.CMvPolynomial.aeval_pow {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (p : CMvPolynomial n R) (k : ℕ) : aeval f (p ^ k) = aeval f p ^ k

@[simp]

theorem CPoly.CMvPolynomial.aeval_neg {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommRing R] [BEq R] [LawfulBEq R] [CommRing σ] [Algebra R σ] (f : Fin n → σ) (p : CMvPolynomial n R) : aeval f (-p) = -aeval f p

@[simp]

theorem CPoly.CMvPolynomial.aeval_sub {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommRing R] [BEq R] [LawfulBEq R] [CommRing σ] [Algebra R σ] (f : Fin n → σ) (p q : CMvPolynomial n R) : aeval f (p - q) = aeval f p - aeval f q

def CPoly.CMvPolynomial.bind₁ {n m : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : CMvPolynomial m R

Substitution: substitutes polynomials for variables.

Given f : Fin n → CMvPolynomial m R, substitutes f i for variable X i.

theorem CPoly.CMvPolynomial.bind₁_eq_aeval {n m : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : bind₁ f p = aeval f p

The computable substitution bind₁ agrees with algebraic evaluation.

@[simp]

theorem CPoly.CMvPolynomial.bind₁_C {n m : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (c : R) : bind₁ f (C c) = C c

@[simp]

theorem CPoly.CMvPolynomial.bind₁_add {n m : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p q : CMvPolynomial n R) : bind₁ f (p + q) = bind₁ f p + bind₁ f q

@[simp]

theorem CPoly.CMvPolynomial.bind₁_mul {n m : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p q : CMvPolynomial n R) : bind₁ f (p * q) = bind₁ f p * bind₁ f q

Core operations

def CPoly.CMvPolynomial.rename {n m : ℕ} {R : Type u_2} [Zero R] [Add R] [BEq R] [LawfulBEq R] (f : Fin n → Fin m) (p : CMvPolynomial n R) : CMvPolynomial m R

Rename variables using a function.

Given f : Fin n → Fin m, renames variable X i to X (f i).

def CPoly.CMvPolynomial.sumToIter {n : ℕ} {R : Type u_2} [Zero R] [Add R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : CMvPolynomial n R

Iterative reconstruction of a polynomial by folding over terms.

Bridge and transport lemmas (technical)

theorem CPoly.CMvPolynomial.X_eq_monomial {k : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (i : Fin k) : X i = monomial (Vector.ofFn fun (j : Fin k) => if j = i then 1 else 0) 1

theorem CPoly.CMvPolynomial.toFinsupp_unitMono {k : ℕ} (i : Fin k) : CMvMonomial.toFinsupp (Vector.ofFn fun (j : Fin k) => if j = i then 1 else 0) = Finsupp.single i 1

theorem CPoly.CMvPolynomial.fromCMvPolynomial_monomial {k : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (mono : CMvMonomial k) (c : R) : fromCMvPolynomial (monomial mono c) = (MvPolynomial.monomial mono.toFinsupp) c

theorem CPoly.CMvPolynomial.fromCMvPolynomial_X {k : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (i : Fin k) : fromCMvPolynomial (X i) = MvPolynomial.X i

C and eval₂ as ring homomorphisms

@[simp]

theorem CPoly.CMvPolynomial.eval₂_C {n : ℕ} {R : Type u_2} {S : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring S] (f : R →+* S) (vs : Fin n → S) (c : R) : eval₂ f vs (C c) = f c

@[simp]

theorem CPoly.CMvPolynomial.eval₂_X {n : ℕ} {R : Type u_2} {S : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring S] (f : R →+* S) (vs : Fin n → S) (i : Fin n) : eval₂ f vs (X i) = vs i

@[simp]

theorem CPoly.CMvPolynomial.eval₂Hom_C {n : ℕ} {R : Type u_2} {S : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring S] (f : R →+* S) (vs : Fin n → S) (c : R) : (eval₂Hom f vs) (C c) = f c

@[simp]

theorem CPoly.CMvPolynomial.eval₂Hom_X {n : ℕ} {R : Type u_2} {S : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring S] (f : R →+* S) (vs : Fin n → S) (i : Fin n) : (eval₂Hom f vs) (X i) = vs i

theorem CPoly.CMvPolynomial.ringHom_ext {n : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] {T : Type u_3} [Semiring T] {f g : CMvPolynomial n R →+* T} (hC : ∀ (c : R), f (C c) = g (C c)) (hX : ∀ (i : Fin n), f (X i) = g (X i)) : f = g

Two ring homomorphisms out of CMvPolynomial n R are equal once they agree on the constants and on every variable.

@[simp]

theorem CPoly.CMvPolynomial.aeval_X {n : ℕ} {R : Type u_2} {σ : Type u_3} [CommSemiring R] [BEq R] [LawfulBEq R] [CommSemiring σ] [Algebra R σ] (f : Fin n → σ) (i : Fin n) : aeval f (X i) = f i

@[simp]

theorem CPoly.CMvPolynomial.bind₁_X {n m : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (i : Fin n) : bind₁ f (X i) = f i

@[simp]

theorem CPoly.CMvPolynomial.bind₁_id {n : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : bind₁ (fun (i : Fin n) => X i) p = p

theorem CPoly.CMvPolynomial.list_foldl_add_comm {β : Type u_2} {K : Type u_3} {V : Type u_4} [AddCommMonoid β] (g : K → V → β) (l : List (K × V)) (init : β) : List.foldl (fun (acc : β) (pair : K × V) => acc + g pair.1 pair.2) init l = List.foldl (fun (acc : β) (pair : K × V) => g pair.1 pair.2 + acc) init l

theorem CPoly.CMvPolynomial.foldl_add_comm {β : Type u_2} [AddCommMonoid β] {k : ℕ} {R' : Type u_3} (g : CMvMonomial k → R' → β) (t : Std.ExtTreeMap (CMvMonomial k) R' compare) : Std.ExtTreeMap.foldl (fun (acc : β) (m : CMvMonomial k) (c : R') => acc + g m c) 0 t = Std.ExtTreeMap.foldl (fun (acc : β) (m : CMvMonomial k) (c : R') => g m c + acc) 0 t

theorem CPoly.CMvPolynomial.fromCMvPolynomial_finsupp_sum {R : Type u_1} {n k : ℕ} [CommSemiring R] [BEq R] [LawfulBEq R] (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R) (a : CMvPolynomial n R) : fromCMvPolynomial ((fromCMvPolynomial a).coeff.sum g) = (fromCMvPolynomial a).coeff.sum fun (μ : Fin n →₀ ℕ) (c : R) => fromCMvPolynomial (g μ c)

API lemmas for sumToIter

theorem CPoly.CMvPolynomial.sumToIter_eq {n : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : p.sumToIter = p

theorem CPoly.CMvPolynomial.coeff_sumToIter {n : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (m : CMvMonomial n) (p : CMvPolynomial n R) : coeff m p.sumToIter = coeff m p

@[simp]

theorem CPoly.CMvPolynomial.sumToIter_zero {n : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] : sumToIter 0 = 0

theorem CPoly.CMvPolynomial.sumToIter_add {n : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (p q : CMvPolynomial n R) : (p + q).sumToIter = p.sumToIter + q.sumToIter

@[simp]

theorem CPoly.CMvPolynomial.sumToIter_idempotent {n : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (p : CMvPolynomial n R) : p.sumToIter.sumToIter = p.sumToIter

theorem CPoly.CMvPolynomial.fromCMvPolynomial_bind₁ {n m : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (f : Fin n → CMvPolynomial m R) (p : CMvPolynomial n R) : fromCMvPolynomial (bind₁ f p) = MvPolynomial.eval₂ MvPolynomial.C (fun (i : Fin n) => fromCMvPolynomial (f i)) (fromCMvPolynomial p)

The computable substitution bind₁ agrees with Mathlib substitution after transporting through fromCMvPolynomial.

Equivalence between npow and npowBySq

Lawful.npow (defined in Multivariate/Lawful.lean) is the naive O(k) specification; Lawful.npowBySq is the O(log k) repeated-squaring implementation. We prove pointwise equality here so that the NatPow instance can be safely routed through the fast version.

The proofs need mul_assoc / mul_one / mul_comm, which are only available once the CommSemiring (CMvPolynomial n R) instance has been built — that is why these lemmas live in Operations.lean rather than in Lawful.lean.

theorem CPoly.Lawful.npow_add {n : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (p : Lawful n R) (a b : ℕ) : npow (a + b) p = npow a p * npow b p

Additive law for the naive npow: $p^{a+b} = p^a \cdot p^b$.

theorem CPoly.Lawful.npowBySq_eq_npow {n : ℕ} {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] (p : Lawful n R) (k : ℕ) : p.npowBySq k = npow k p

The fast repeated-squaring npowBySq agrees pointwise with the naive npow. This is the equivalence that lets the NatPow (Lawful n R) instance be routed through npowBySq without changing observable behavior.