Add some correspondences with mathlib

[ErVinuelas]

Added correspondence with mathlib for a couple of functions, as requested in the TO-DO of the file.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Add some correspondences with mathlib

Mathematical Formalization

• New lemmas connecting CompPoly to mathlib:
  • degreeOf_restrictDegree_le: bounds the per-variable degree of restrictDegree.
  • fromCMvPolynomial_restrictTotalDegree_mem: shows fromCMvPolynomial maps the custom restrictTotalDegree submodule into mathlib's MvPolynomial.restrictTotalDegree submodule.
  • fromCMvPolynomial_restrictDegree_mem: shows fromCMvPolynomial maps the custom restrictDegree submodule into mathlib's MvPolynomial.restrictDegree submodule.
• Removed TODO block: The file's previous TODO block (requesting these correspondences) has been removed, indicating these additions complete that task.

Infrastructure / CI

• New imports: CompPoly.Multivariate.MvPolyEquiv and Mathlib.RingTheory.MvPolynomial.Basic were added to support the new lemmas.

Note: The PR body is minimal and does not detail the per-file changes. The actual code changes are accurately reflected in the per-file summary above. No new sorry or admit placeholders were introduced.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	35
❌ Lines Removed	5

---

Lean Declarations

✏️ Added: 3 declaration(s)

CompPoly/Multivariate/Restrict.lean (3)

• lemma degreeOf_restrictDegree_le (d : ℕ) (p : CMvPolynomial n R) (i : Fin n) :
• theorem fromCMvPolynomial_restrictDegree_mem {R : Type*} [CommSemiring R] [BEq R]
• theorem fromCMvPolynomial_restrictTotalDegree_mem {R : Type*} [CommSemiring R] [BEq R]

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Style guide violations found; primarily line-length issues. The diff otherwise follows naming, documentation, and formatting conventions.

---

📄 **Per-File Summaries**

• CompPoly/Multivariate/Restrict.lean: Added degreeOf_restrictDegree_le lemma bounding the per-variable degree of restrictDegree. Removed the TODO block and added two correctness theorems—fromCMvPolynomial_restrictTotalDegree_mem and fromCMvPolynomial_restrictDegree_mem—which show that fromCMvPolynomial maps the custom restrictTotalDegree and restrictDegree into Mathlib's MvPolynomial.restrictTotalDegree and MvPolynomial.restrictDegree submodules, respectively. The new imports CompPoly.Multivariate.MvPolyEquiv and Mathlib.RingTheory.MvPolynomial.Basic support these additions.

---

Last updated: 2026-07-23 12:23 UTC.

[dhsorens]

thanks @ErVinuelas ! happy to merge once the checks pass