Omitted variables are… to Comparison with Lagrange…

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

TheoremOmitted variables are algebraically independent over the source fraction ring#

For a commutative domain R, an injective map ρ : τ → σ, and arbitrary commutative-ring fraction rings L of MvPolynomial τ R and K of MvPolynomial σ R, MvPolynomial.algebraicIndependent_fractionRing_map_rename_compl proves that the images of X i in K, indexed by {i : σ // i ∉ Set.range ρ}, are algebraically independent over L. The L-algebra structure on K must be induced by the same canonical fraction-ring map of MvPolynomial.rename ρ, not an arbitrary scalar action. The five universes of R, τ, σ, L and K are independent; no Field instances or finite index types are required.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.algebraicIndependent_fractionRing_map_rename_compl

TheoremOmitted variables form a transcendence basis over the source fraction ring#

In the same five-universe commutative-domain setting and under the full canonical fraction-renaming scalar action, MvPolynomial.isAlgebraic_adjoin_fractionRing_map_rename_compl proves that K is algebraic over the L-subalgebra generated by the complementary localized variables, and MvPolynomial.isTranscendenceBasis_fractionRing_map_rename_compl identifies that family as a transcendence basis over L. Under the same hypotheses, MvPolynomial.isFractionRing_adjoin_fractionRing_map_rename_compl makes K the fraction ring of that generated L-subalgebra, for its canonical inclusion into K. The adjoin is over the source fraction ring, not the coefficient ring. Neither fraction-ring realization needs a Field instance, and neither variable type need be finite. The direct-import examples include the nonempty complement of Unit → Bool, () ↦ false, over ℤ, as well as arbitrary fraction-ring realizations.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.isAlgebraic_adjoin_fractionRing_map_rename_compl

Zeros are closed points of polynomial quotients. For any ideal I in MvPolynomial σ K with K algebraically closed and σ finite, the canonical point-set equivalence identifies MvPolynomial.zeroLocus K I with closed points of the spectrum of MvPolynomial σ K ⧸ I. The forward prime is the kernel of descended evaluation; polynomial membership and inverse coordinates have explicit laws. The field and variables may inhabit different universes, and I may be the unit ideal or define a nonreduced quotient. This point-set result itself does not assert a topological or sheaf equivalence.

TheoremThe image of evaluating one polynomial at two points#

Over any commutative ring R, for assignments a b : σ → R with independent coefficient and variable universes, MvPolynomial.mem_range_eval_prod_iff characterizes value pairs (r, s) : R × R of one common polynomial by r - s ∈ Ideal.span (Set.range (fun i => a i - b i)), without a finite-variable, field or comaximality assumption. The examples contrast same-parity pairs at the one-variable integer points 0 and 2 with all pairs at the two-variable points (0, 0) and (2, 3) despite nonunit coordinate differences, and include empty-variable diagonal and zero-ring boundaries.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.mem_range_eval_prod_iff

TheoremFinite simultaneous polynomial evaluation has an exact surjectivity criterion#

For any commutative ring R, arbitrary variable type σ, finite point-index type ι and family a : ι → σ → R, MvPolynomial.surjective_eval_family_iff states that p ↦ (i ↦ MvPolynomial.eval (a i) p) is surjective exactly when the coordinate differences a i s - a j s, for all s : σ, generate the unit ideal for every pair of distinct indices i ≠ j. The three types have independent universes. Empty families, empty or infinite variable types, repeated points and the zero ring are included; no field hypothesis is needed.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.surjective_eval_family_iff

TheoremEvaluation-kernel powers are detected by translated coefficients#

For any commutative semiring R and point a : σ → AddUnits R, MvPolynomial.mem_pow_ker_eval_addUnits_iff characterizes membership in every nth evaluation-kernel power by vanishing of all coefficients of total degree < n after the translation p(X + a). Over a commutative ring, MvPolynomial.mem_pow_ker_eval_iff allows arbitrary points a : σ → R. Both results allow arbitrary variable types, independent coefficient/variable universes, and every n : ℕ, including zero.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.mem_pow_ker_eval_addUnits_iff

Separated polynomial point quotients are square-zero extensions. Over any commutative ring, including the zero ring, and any index type, the generator-prescribed forward map from the quotient by coordinate squares and point relations is bijective when differences of distinct evaluation points are units. The resulting polynomial-algebra equivalence has forward coordinate laws and an inverse law on the evaluation summands; no mixed-product relations are added to the defining ideal. See the API guide for the two modules and their boundary examples.

Subset-weight-one valuations have full rational residue fields. For any field, any variable type and subset containing a chosen pivot, the weight-one construction identifies the multivariate function field birationally with a univariate rational function field over the field of unweighted variables and pivot ratios. Minimum subset weight gives a surjective rank-one discrete valuation; its pivot is a uniformizer, and its entire residue field is the rational function field in those unweighted variables and ratios. The equal-order fraction law computes residues from initial coefficients. For the empty subset, the separate trivial valuation has no discrete-valuation claim.

TheoremHilbert basis theorem for left-Noetherian rings#

Polynomial.isNoetherianRing_of_isNoetherianRing proves IsNoetherianRing (Polynomial R) for any R : Type u with [Ring R] and [IsNoetherianRing R]. The polynomial variable is central; coefficient commutativity, nontriviality and absence of zero divisors are not required. On commutative rings, Polynomial.isNoetherianRing_of_isNoetherianRing_eq_isNoetherianRing identifies this proof with Mathlib's Polynomial.isNoetherianRing. For any finite type σ : Type v, the named theorem AddMonoidAlgebra.isNoetherianRing_finsupp proves left Noetherianity of AddMonoidAlgebra R (σ →₀ ℕ), with independently polymorphic universes. It permits zero and noncommutative coefficient rings. For commutative rings, this is definitionally MvPolynomial σ R. Here IsNoetherianRing R means IsNoetherian R R for the canonical left self-action. It does not assume IsNoetherian R (Polynomial R): that coefficient-module property is false for every nontrivial coefficient ring. The examples include the noncommutative 16-element ring Matrix (Fin 2) (Fin 2) (ZMod 2), whose polynomial ring is infinite but left-Noetherian, the zero ring ZMod 1, and ZMod 4 with its nonzero nilpotent 2.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanPolynomial.isNoetherianRing_of_isNoetherianRing

Noetherian polynomial-ring criteria. The Noetherian module proves the coefficient-and-variable characterization over arbitrary commutative rings: MvPolynomial σ R is Noetherian for its self-action exactly when R is Noetherian and either σ is finite or R is the zero ring. For nontrivial commutative semirings, Noetherianity of the polynomial semiring forces σ to be finite; no semiring Hilbert-basis sufficiency is asserted. The nontrivial-ring form removes the zero-ring alternative without imposing a domain hypothesis. The coefficient and variable universes are independent. The examples distinguish empty, finite and infinite variables over the integers, ZMod 6, and ZMod 1.

TheoremArtinian polynomial-semiring criteria#

For any R : Type u with [Semiring R], including noncommutative coefficients, Polynomial.isArtinianRing_iff proves IsArtinianRing (Polynomial R) ↔ Subsingleton R. For arbitrary variable types σ : Type u and coefficients R : Type v with [CommSemiring R], MvPolynomial.isArtinianRing_iff proves IsArtinianRing (MvPolynomial σ R) ↔ IsArtinianRing R ∧ (IsEmpty σ ∨ Subsingleton R). Both use polynomial multiplication on the canonical left self-module, not the coefficient R-module action. All universes are arbitrary; the multivariate universes are independent. No ring or finite-variable hypothesis is imposed. Empty multivariate variables recover coefficient Artinianity; trivial coefficients make every polynomial zero. The univariate applications include the usual non-ring semiring ℝ≥0, the noncommutative 16-element matrix ring over ZMod 2, and the zero ring ZMod 1.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanPolynomial.isArtinianRing_iff

TheoremUnivariate coefficient-module Noetherianity and Artinianity each characterize trivial coefficients#

For any R : Type u with [Semiring R], Polynomial.isNoetherian_iff and Polynomial.isArtinian_iff give IsNoetherian R (Polynomial R) ↔ Subsingleton R and IsArtinian R (Polynomial R) ↔ Subsingleton R, respectively. Both use the canonical left coefficient action r • p = Polynomial.C r * p, not polynomial multiplication as a self-module. The universe is arbitrary; no commutativity, ring, domain or field hypothesis is required. The coefficient-module examples distinguish these properties from coefficient self-Noetherianity and self-Artinianity, even for the infinite non-ring semiring ℝ≥0 with finitely many ideals.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanPolynomial.isNoetherian_iff

TheoremRadical coefficient-ideal extensions are characterized by subtractivity#

For any commutative semiring R, ideal I, and nonempty variable type σ, MvPolynomial.isRadical_map_C_iff says that I.map C is radical exactly when I is radical and satisfies a ∈ I → a + b ∈ I → b ∈ I. The sufficiency theorem also allows empty variable types. The coefficient and variable universes are independent; no properness, ring, domain, reducedness or finiteness hypothesis is needed. The examples include the proper nonzero kernel of reduction ℕ →+* ZMod 2 and the original prime-extension and radical-extension necessity applications.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.isRadical_map_C_iff

TheoremCoefficient-and-variable ideals have an exact finite-generation criterion#

For any commutative semiring R, coefficient ideal I, and variable subset S, MvPolynomial.ideal_map_C_sup_span_X_image_fg_iff characterizes finite generation of Ideal.map C I ⊔ Ideal.span (X '' S): I must be finitely generated, and either S is finite or I is the unit ideal. The coefficient and variable universes are independent; no ring, domain, subtractivity or finite-ambient-variable hypothesis is required. The examples include a proper nonsubtractive ideal over ℕ, coefficient zero divisors, and the zero-ring boundary.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.ideal_map_C_sup_span_X_image_fg_iff

TheoremThe variable ideal is not finitely generated#

For a nontrivial commutative semiring and infinitely many variables, MvPolynomial.idealOfVars_not_fg proves non-finite generation. A finite union of polynomial supports misses some variable; evaluation separating that variable gives a contradiction. Mathlib supplies the complementary finite-variable ideal theorem. This library does not prove the motivating complete short exact sequence.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.idealOfVars_not_fg

DefinitionAntichain coefficients of monomial ideals#

For any commutative semiring R, arbitrary variable type σ and antichain S : Set (σ →₀ ℕ), MvPolynomial.monomialIdealCoeffMap restricts coefficients from the stock ideal generated by the monic monomials with exponents in S to S →₀ R. It is surjective and semilinear over constantCoeff, for the full polynomial-semiring action on the ideal and the coefficient action on the target. Its coordinate and monomial laws give the original coefficients and the corresponding single functions. Coefficients and variables have independent universes; empty or infinite antichains and variable types, and trivial coefficients, are allowed. The coordinate-axes example records the three exponents of (xy, xz, yz) over ℂ, their antichain and monomial presentation, and the ideal's nonzeroness and properness. For finite S and nontrivial R, MvPolynomial.spanFinrank_ideal_span_monomial proves that the ideal's minimum number of polynomial generators is S.ncard. MvPolynomial.card_le_card_of_span_eq_ideal_span_monomial bounds every finite generating set, not only sets of monomials. This is generation over the full polynomial semiring, not coefficient-module dimension. The coordinate-axes example consequently has minimum number of generators three.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.monomialIdealCoeffMap

DefinitionVariable classes form the augmentation cotangent basis#

For any (σ : Type u) and (R : Type v) [CommRing R], MvPolynomial.idealOfVarsCotangentBasis is a σ-indexed R-basis of the stock variable-ideal cotangent I/I². Its vectors are the classes of X i, with inherited coefficient action r • [p] = [C r * p]. The _apply and _repr_X lemmas characterize those vectors, and idealOfVarsCotangentBasis_repr_toCotangent computes each coordinate as (x : MvPolynomial σ R).coeff (Finsupp.single i 1) for any representative x in the variable ideal. Quadratic and higher terms do not contribute. The variable and coefficient universes are independent; empty or infinite variable types, zero rings and nilpotent coefficients are allowed. This is an indexed basis, not a numerical rank assertion over the zero ring.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.idealOfVarsCotangentBasis

TheoremDegree-controlled finite interpolation#

Over any commutative ring R, let s : Finset ι select points a : ι → σ → R. If, for every distinct i, j ∈ s, the coordinate differences a i x - a j x span the unit ideal, then any prescribed values v : ι → R are attained on s by a polynomial of total degree at most s.card - 1 (MvPolynomial.exists_eval_eq_totalDegree_le_of_pairwise_span_eq_top). Both the variable type and ambient label type may be infinite; no field or domain hypothesis is needed. The theorem asserts existence, not uniqueness.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.exists_eval_eq_totalDegree_le_of_pairwise_span_eq_top

TheoremComparison with Lagrange interpolation#

Over a field, for a unique variable type, a polynomial taking prescribed values at distinct nodes and having total degree strictly below the number of nodes maps to Mathlib's Lagrange interpolant under the canonical single-variable equivalence (MvPolynomial.uniqueAlgEquiv_eq_interpolate_of_eval_eq). The univariate degree bound follows from the total-degree bound. On a nonempty selection, the bound s.card - 1 also suffices, so the comparison applies to any bounded witness supplied by the commutative-ring existence theorem. Zero agrees with the empty interpolant separately; an arbitrary degree-zero witness need not do so.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.uniqueAlgEquiv_eq_interpolate_of_eval_eq

The full results guide also covers simultaneous finite-fraction origins and their preimage dimension bounds, polynomial Zariski topology, valuation naturality, evaluation kernels, coefficient-module Noetherianity and Artinianity, polynomial self-Artinianity, and the substitution, degree, division and lifting interfaces, with all their hypotheses and boundary cases. Its fraction examples explain how to use the common finite stage and why whole stage fields do not provide the subsemiring dimension bound.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.