Multivariate polynomials

Reusable multivariate-polynomial results on infinite-variable ideals, coordinate-difference evaluation ideals, polynomial maximal-spectrum infinitude and the classification of univariate polynomial closed points by algebraic-closure automorphism orbits without separability, normal-extension automorphism orbits as minimal-polynomial root sets with cardinality equal to separable degree and full degree exactly for separable elements, homogeneous evaluation, disjoint-block substitution and its iteration, finite-variable origins of finite collections of polynomial fractions over integral domains in arbitrary fraction-ring representations, and a Krull-dimension bound for subsemirings by their finite-variable fraction-stage preimage dimensions, not the whole stage fields, degree, coefficient extraction and linear evaluation, chosen linear division, existential monic lifts and scalar-top first-variable lex degree. The univariate Hilbert basis theorem holds for any left-Noetherian ring, without coefficient commutativity, using a central variable and the canonical left self-module. The same holds for finitely many central natural-number coordinates via AddMonoidAlgebra, with independent coefficient and coordinate universes. Central Laurent polynomial rings over left-Noetherian rings are likewise left-Noetherian, including noncommutative and zero coefficient rings. The Laurent argument clears negative exponents by units and reuses the arbitrary-ring polynomial theorem. A polynomial point quotient by indexed squares and linear point relations has a canonical map to a square-zero extension of evaluation quotients; that same map is an algebra equivalence under pairwise unit differences. See README.md and docs/API.md for precise hypotheses and limitations.

Quoted from the project description in formalization.yaml of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

55 articles: 55 for headline results in its README whose declaration link names a declaration the scan finds in the linked file. Its other headline results are quoted where they stand.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

• Repository: FormalFrontier/multivariate-polynomials, read at commit 724d9804 (2026-11-05).
• Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
• License: Apache-2.0.
• Authors: Formal Frontier Agents.
• Review status: “Review evidence is revision-specific”.
• Review notes: “Independent review, builds and axiom audits apply only to the declarations and exact source revisions they cover. This metadata does not certify a successful build or complete standard-axiom audit for every selected result, nor does it establish source-specific correspondence.”
• Automation: agent; tool setup “Formal Frontier AI agents used Lean, Lake and mathlib for proof development, examples and documentation, with independent review.”
• Automation notes: “Mathlib's polynomial, ideal and finitely supported-function APIs support the degree, coefficient, substitution and division results. Their statements specify the relevant coefficient and order hypotheses.”

Literature

The sources its formalization.yaml names, with their relationship to it.

• Mathlib, Mathlib Contributors, https://github.com/leanprover-community/mathlib4 (software; background).
• Minimal Primes, Formal Frontier Agents, https://github.com/FormalFrontier/minimal-primes/tree/c069147fd1754e4a87be7e09003439f1d2250bfd (software; background).
• Algebraic Direct Limits, Formal Frontier Agents, https://github.com/FormalFrontier/algebraic-direct-limits/tree/5959888b3d648cf1f72038459f63d804093d6c54 (software; background).
• Foundations of Rigid Geometry I, Kazuhiro Fujiwara, Fumiharu Kato, arXiv:1308.4734v5 (book; background).
• A non-finitely-generated variable ideal: finite-support proof exposition, Formal Frontier Agents (original-proof; adapts).
• The Rising Sea: Foundations of Algebraic Geometry, Ravi Vakil, October 21, 2025 draft, Exercise 6.7.E, PDF page 199 (book; background).
• Structural block substitution and the two iteration orders, Beacon (original-proof; adapts).
• Exact total degree of substitution into disjoint blocks, Formal Frontier Agents (original-proof; adapts).
• Polynomial-parameter coefficients of homogeneous multivariate polynomials, Formal Frontier Agents (original-proof; background).
• Polynomial equations in finite-basis coordinates, Beacon (original-proof; background).

Builds on

• Algebraic direct limits (a Lake dependency, pinned at 5959888b)
• Coherent modules (a Lake dependency, pinned at e848789e)
• Group theory (a Lake dependency, pinned at 41da4c03)
• Minimal primes (a Lake dependency, pinned at c069147f)

Used by

• Adic modules
• Algebraic groups
• Formal power series
• Group rings
• Norm forms
• Scheme properties
• Toric ideals
• Valuation integers

Heights of homogeneous… to Jacobson radicals of…

• Heights of homogeneous polynomial evaluations
• Homogeneous polynomial maps on projective coordinate spaces
• Polynomial closed points and algebraic-closure orbits
• Infinitely many maximal ideals of polynomial rings
• Factorization uniqueness from a regular crossed resultant
• Nonconstant coefficients of polynomial units
• Polynomial units over commutative semirings
• Prime coefficient extensions over commutative semirings
• Maximal coefficient extensions over commutative semirings
• Finite coefficient-product equations determine whole products
• Radicals of coefficient-ideal extensions
• Scalar annihilators and non-zero-divisors
• The degree-zero homogeneous component
• Coefficient ideals over commutative semirings
• Square witnesses for failure of subtractivity
• Powers of augmented coefficient ideals
• Primary coefficient ideals
• Supplied primary families and deletion irredundance
• Nilpotent coefficients and irreducible polynomial spectra
• Jacobson radicals of coefficient ideals

Integral elements over… to Fraction-ring renaming is…

• Integral elements over coefficient rings
• Integral closure in arbitrarily many variables
• Flatness of commutative-ring variable renaming
• Canonical unique-variable degree
• Injectivity and surjectivity of variable renaming
• Formal smoothness of variable renaming
• Smoothness of variable renaming
• Formal unramifiedness of variable renaming
• Integrality of polynomial variable renaming
• Algebraicity of polynomial variable renaming
• Finite presentation of commutative-ring variable renaming
• Zero-variable presentations and semiring renaming
• Variable renaming has an exact relative finite-type criterion
• Variable renaming has an exact relative essentially finite-type criterion
• Module finiteness of variable renaming has a sharper criterion
• Quasi-finiteness of commutative-ring variable renaming
• Finite coefficient aggregation has an exact injectivity criterion
• Joint degree-and-support profiles recover bivariate coefficients only for trivial coefficients
• Variable-renaming kernels have an exact presentation and finite-generation criterion
• Fraction-ring renaming is surjective, equivalently integral, exactly when it covers all variables

Omitted variables are… to Comparison with Lagrange…

• Omitted variables are algebraically independent over the source fraction ring
• Omitted variables form a transcendence basis over the source fraction ring
• The image of evaluating one polynomial at two points
• Finite simultaneous polynomial evaluation has an exact surjectivity criterion
• Evaluation-kernel powers are detected by translated coefficients
• Hilbert basis theorem for left-Noetherian rings
• Artinian polynomial-semiring criteria
• Univariate coefficient-module Noetherianity and Artinianity each characterize trivial coefficients
• Radical coefficient-ideal extensions are characterized by subtractivity
• Coefficient-and-variable ideals have an exact finite-generation criterion
• The variable ideal is not finitely generated
• Antichain coefficients of monomial ideals
• Variable classes form the augmentation cotangent basis
• Degree-controlled finite interpolation
• Comparison with Lagrange interpolation

Main results

Its formalization.yaml lists 54 main results, and the scan finds 54 of them declared in the file the yaml gives; they are on their own page, not made articles.

• Main results

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.