feat(bivariate): Add commutativity of bivariate evaluation

[ElijahVlasov]

No description provided.

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Establishes commutativity of evaluation for bivariate polynomials over a commutative semiring via the eval_comm theorem.
• Proves that evaluating in $X$ then $Y$ yields the same result as evaluating in $Y$ then $X$.
• Adds BivariateEvaluation.lean with complete proofs and no sorry placeholders.

Integration and Infrastructure

• Placed within the ToMathlib directory as a general-purpose library extension.
• Updated CompPoly.lean imports to integrate the new functionality.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	46
❌ Lines Removed	0

---

Lean Declarations

✏️ **Added:** 1 declaration(s)

• theorem eval_comm {f : Polynomial (Polynomial F)} {a x : F} : in CompPoly/ToMathlib/Polynomial/BivariateEvaluation.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following style guide violations were found in CompPoly/ToMathlib/Polynomial/BivariateEvaluation.lean:

• Line 23: variable {F : Type*} violates "Put spaces on both sides of :, :=, and infix operators." (missing space before :).
• Line 23: Variable name F violates "α, β, γ, ... : Generic types".
• Line 31: Variable name F violates "α, β, γ, ... : Generic types".
• Line 32: Variable name f violates "x, y, z, ... : Elements of a generic type".
• Line 32: Variable name a violates "a, b, c, ... : Propositions" (used here for an element of a ring).
• Line 35: have h_eval : violates "Put spaces on both sides of :, :=, and infix operators." (missing space before :).
• Line 37: Variable name i violates "m, n, k, ... : Natural numbers" and "i, j, k, ... : Integers" (polynomial coefficient indices are natural numbers).
• Line 38: The empty line inside the proof of eval_comm violates "Avoid empty lines inside definitions or proofs."
• Line 40: The 8-space indentation for the continuation of the simp tactic violates "Use 2 spaces for indentation."

---

📄 **Per-File Summaries**

• CompPoly.lean: This update adds an import for bivariate polynomial evaluation to the main file of the CompPoly library. This modification integrates new functionality for handling bivariate evaluations into the project's core.
• CompPoly/ToMathlib/Polynomial/BivariateEvaluation.lean: This file introduces the theorem eval_comm, which establishes the commutativity of evaluation for bivariate polynomials in a commutative semiring. The result proves that evaluating a polynomial in $X$ and then $Y$ is equivalent to evaluating in $Y$ first and then in $X$ using complete proofs without placeholders.

---

Last updated: 2026-04-23 17:05 UTC.

[dhsorens]

thanks for the PR @ElijahVlasov ! I'm happy in principle to have this result, although it might be more interesting if you proved the computable version in Bivariate/Basic.lean if you're up to the challenge! (this lemma may be useful for that)

the result may be good to have, but I don't think that it needs its own file. if you're happy to refactor this into ToMathlib/Polynomial/BivariateDegree.lean and get it passing the linter we can merge.